diff --git a/CSPM-ToProlog.cabal b/CSPM-ToProlog.cabal
--- a/CSPM-ToProlog.cabal
+++ b/CSPM-ToProlog.cabal
@@ -1,5 +1,5 @@
 Name:                CSPM-ToProlog
-Version:             0.3.1.0
+Version:             0.4.0.0
 Synopsis:            some modules specific for the ProB tool
 Description:
   This package constains a translation from a CSPM AST to the representation
@@ -11,15 +11,14 @@
 License-File:        LICENSE
 Author:              2006-2011 Marc Fontaine
 Maintainer:          Marc Fontaine <fontaine@cs.uni-duesseldorf.de>
-HomePage:            http://www.stups.uni-duesseldorf.de/ProB
 Cabal-Version:  >= 1.10
-Tested-With:    GHC==7.0.2
+Tested-With:    GHC==7.0.3
 Build-Type:     Simple
 
 Library
   Default-Language: Haskell2010
   Build-Depends:
-    CSPM-Frontend >= 0.6 && < 0.7
+    CSPM-Frontend >= 0.7 && < 0.8
     ,pretty >= 1.0 && < 1.1
     ,base >= 4.0 && <5.0
     ,containers >= 0.4 && <0.5
diff --git a/src/Language/CSPM/AstToProlog.hs b/src/Language/CSPM/AstToProlog.hs
--- a/src/Language/CSPM/AstToProlog.hs
+++ b/src/Language/CSPM/AstToProlog.hs
@@ -21,7 +21,7 @@
 )
 where
 
-import Language.CSPM.Frontend (ModuleFromRenaming)
+import Language.CSPM.Frontend (ModuleFromRenaming, frontendVersion)
 import Language.CSPM.AST
 import qualified Language.CSPM.SrcLoc as SrcLoc
 import Language.Prolog.PrettyPrint.Direct
@@ -30,26 +30,28 @@
 import Data.Set (Set)
 import qualified Data.Set as Set
 import qualified Data.IntMap as IntMap
+import Data.Version
 
 -- | Translate a "LModule" into a "Doc" containing a number of Prolog facts.
 -- The LModule must be a renamed,i.e. contain only unique "Ident"ifier.
 cspToProlog ::
   ModuleFromRenaming -- ^ the renamed Module
   -> Doc  -- ^ prolog facts
-cspToProlog ast = 
-  let
-     core = mkModule ast
-     header = 
-       (text ":- dynamic channel/2, bindval/3, agent/3.")
-       $+$ 
-       (text ":- dynamic agent_curry/3, symbol/4.")
-       $+$ 
-       (text ":- dynamic dataTypeDef/2, subTypeDef/2, nameType/2.")
-       $+$
-       (text ":- dynamic cspTransparent/1.")
-       $+$
-       (text ":- dynamic cspPrint/1.")
-   in header $+$ core
+cspToProlog ast = header $+$ core
+  where
+    core = mkModule ast
+    header = vcat [
+         text ":- dynamic parserVersionNum/1, parserVersionStr/1."
+        ,text ":- dynamic channel/2, bindval/3, agent/3."
+        ,text ":- dynamic agent_curry/3, symbol/4."
+        ,text ":- dynamic dataTypeDef/2, subTypeDef/2, nameType/2."
+        ,text ":- dynamic cspTransparent/1."
+        ,text ":- dynamic cspPrint/1."
+        ,text ":- dynamic pragma/1."
+        ,text ":- dynamic comment/2."
+        ,text ":- dynamic assertBool/1, assertRef/5, assertTauPrio/6."
+        ,text ":- dynamic assertModelCheckExt/4, assertModelCheck/3."
+        ]
 
 plLocatedConstructs :: Set Const
 plLocatedConstructs = Set.fromList 
@@ -59,8 +61,27 @@
 
 mkModule :: ModuleFromRenaming -> Doc
 mkModule m
-  = plPrg [declGroup $ map clause $ declList $ moduleDecls m]
+  = plPrg [
+      singleClause $ clause $ nTerm "parserVersionNum"
+        [pList $ map atom $ versionBranch $ frontendVersion]
+     ,singleClause $ clause $ nTerm "parserVersionStr"
+        [atom ("CSPM-Frontent-" ++ showVersion frontendVersion)]
+     ,declGroup $ map clause $ declList $ moduleDecls m
+     ,declGroup $ map mkPragma  $ modulePragmas m
+     ,declGroup $ map mkComment $ moduleComments m
+     ]
 
+mkPragma :: String -> Clause
+mkPragma s = clause $ nTerm "pragma" [aTerm s]
+
+mkComment :: (Comment, SrcLoc.SrcLoc) -> Clause
+mkComment (c, loc) = clause $ nTerm "comment" [com, mkSrcLoc loc]
+  where
+    com = case c of
+      LineComment s ->  nTerm "lineComment" [aTerm s]
+      BlockComment s -> nTerm "blockComment" [aTerm s]
+      PragmaComment s -> nTerm "pragmaComment" [aTerm s]
+
 te :: LExp -> Term
 te expr = case unLabel expr of
   Var i -> let u = unUIdent $ unLabel i in
@@ -94,7 +115,6 @@
   Events -> aTerm "Events"
   BoolSet -> aTerm "boolType"
   IntSet  -> aTerm "intType"
-  ProcSet -> aTerm "procType"
   TupleExp i -> nTerm "tupleExp" [eList i]
   Parens e -> term $ te e
   AndExp a b -> nTerm "bool_and" [te a, te b]
@@ -103,7 +123,7 @@
   NegExp a -> nTerm "negate" [te a]
   Fun1 op a -> nTerm (builtInToString op) [te a]
   Fun2 op a b -> if ((unBuiltIn op) `Set.member` plLocatedConstructs ) 
-    then nTerm (builtInToString op) [te a, te b, plLoc expr]
+    then nTerm (builtInToString op) [te a, te b, nTerm "src_span_operator" [plLoc expr, plLoc op]]
     else nTerm (builtInToString op) [te a, te b]
   DotTuple a -> nTerm "dotTuple" [eList a]
   Closure l -> nTerm "closure" [ eList l]
@@ -222,11 +242,11 @@
       [p] -> nTerm "agent" [
               nTerm (plName ident) $ map tp p
              ,te e
-             ,plLoc ident]
+             ,plLoc e]
       l -> nTerm "agent_curry" [
               nTerm (plName ident) $ map (pList . map tp) l 
              ,te e
-             ,plLoc ident]
+             ,plLoc e]
     mkFunBind _ (FunCaseI {}) = error "unexpected case in mkFunBind: FunCaseI"
     mkConstructorList :: [LConstructor] -> Term
     mkConstructorList l = pList $ map mkConstructor l
@@ -260,25 +280,20 @@
     termShow :: Show a => Labeled a -> Term
     termShow = aTerm . show . unLabel
 
-plName :: LIdent -> Atom
-plName l
-  = let uIdent = unUIdent $ unLabel l in case idType uIdent of
-    TransparentID -> atom $ realName uIdent
-    VarID         -> error ("plName : " ++ show l)
-    _             -> atom $ uniquePlName uIdent
-
 plNameTerm :: LIdent -> Term
 plNameTerm l
   = let uIdent = unUIdent $ unLabel l in case (idType uIdent,prologMode uIdent) of
     (VarID,PrologVariable) -> plVar ("_" ++ uniquePlName uIdent)
     (VarID,PrologGround)   -> term $ atom $ uniquePlName uIdent
     _             -> term $ plName l
-{-
-{- fix me , temporal hack, switchoff renaming for channel,etc-}
-    (FunID _,_)   -> term $ atom $ uniquePlName uIdent
-    (_,_)         -> term $ atom $ uniquePlName uIdent -- <- TODO,FIX BUG
--}
 
+plName :: LIdent -> Atom
+plName l
+      = let uIdent = unUIdent $ unLabel l in case idType uIdent of
+       TransparentID -> atom $ realName uIdent
+       VarID         -> error ("plName : " ++ show l)
+       _             -> atom $ uniquePlName uIdent
+
 uniquePlName :: UniqueIdent -> String
 uniquePlName i = newName i
 
@@ -333,15 +348,14 @@
   pprintIDType i = case idType i of
     ChannelID -> "Channel"
     NameTypeID -> "Nametype"
-    (FunID x) -> "Funktion or Process ( Arity :"++show x ++")"
-    (ConstrID d)   -> "Constructor of Datatype "++d
+    FunID -> "Funktion or Process"
+    ConstrID   -> "Constructor of Datatype"
     DataTypeID     -> "Datatype"
     TransparentID  -> "Transparent function"
+    BuiltInID  -> "BuiltIn primitive"
     VarID -> case prologMode i of
       PrologGround -> "Ident (Groundrep.)"
       PrologVariable -> "Ident (Prolog Variable)"
-
-
 
 -- | Map the abstract datatype LBuiltIn back to plain Strings for Prolog
 builtInToString :: LBuiltIn -> String
diff --git a/src/Language/CSPM/TranslateToProlog.hs b/src/Language/CSPM/TranslateToProlog.hs
--- a/src/Language/CSPM/TranslateToProlog.hs
+++ b/src/Language/CSPM/TranslateToProlog.hs
@@ -3,7 +3,7 @@
 -- Module      :  Language.CSPM.TranslateToProlog
 -- Copyright   :  (c) Fontaine 2010 - 2011
 -- License     :  BSD3
--- 
+--
 -- Maintainer  :  fontaine@cs.uni-duesseldorf.de
 -- Stability   :  experimental
 -- Portability :  GHC-only
@@ -27,6 +27,7 @@
 
 import Control.Exception
 import System.Exit
+import System.IO
 import System.CPUTime
 import Text.PrettyPrint
 
@@ -44,10 +45,10 @@
                $ handleRenameError renameErrorHandler $ mainWork inFile
   (r :: Either SomeException ()) <- try $ writeFile outFile res
   case r of
-    Right () -> return ()
+    Right () -> exitSuccess
     Left err -> do
-      putStrLn "output-file not written"
-      putStrLn $ show err
+      hPutStrLn stderr "output-file not written"
+      hPutStrLn stderr $ show err
       exitFailure
 
 {-
@@ -80,7 +81,7 @@
   printDebug $ "parsetime : " ++ showTime(time_have_ast - time_have_tokens)
   
   time_start_renaming <- getCPUTime
-  (astNew,renaming) <- eitherToExc $ renameModule ast
+  (astNew, renaming) <- eitherToExc $ renameModule ast
   let
     plCode = cspToProlog astNew
     symbolTable = mkSymbolTable $ identDefinition renaming
diff --git a/src/Language/Prolog/PrettyPrint/Direct.hs b/src/Language/Prolog/PrettyPrint/Direct.hs
--- a/src/Language/Prolog/PrettyPrint/Direct.hs
+++ b/src/Language/Prolog/PrettyPrint/Direct.hs
@@ -3,7 +3,7 @@
 -- Module      :  Language.Prolog.PrettyPrint.Direct
 -- Copyright   :  (c) Fontaine 2010 - 2011
 -- License     :  BSD3
--- 
+--
 -- Maintainer  :  fontaine@cs.uni-duesseldorf.de
 -- Stability   :  experimental
 -- Portability :  GHC-only
@@ -30,6 +30,7 @@
 
 import Text.PrettyPrint
 import Data.Char
+import Numeric (showHex)
 
 renderProlog :: Doc -> String
 renderProlog a = renderStyle (Style PageMode 60 1.5) a
@@ -51,11 +52,6 @@
 instance ATOM Double where atom = Atom . double 
 instance ATOM Quote where atom (Quote s) = Atom $ text $ quoteString s
 
-quoteString :: String -> String
-quoteString a 
-  = "'"++(escapeQuote $ tail $ reverse $ tail $ reverse $ show a )++"'"
-
-
 class TERM t where term :: t -> Term
 
 instance TERM Term where term = id
@@ -138,7 +134,16 @@
 plPrg :: [Decl] -> Doc
 plPrg l = vcat $ map unDecl l
 
-escapeQuote :: String -> String
-escapeQuote x = concatMap escapeQ x
-  where escapeQ '\'' = "\\'"
-        escapeQ c = [c]
+quoteString :: String -> String
+quoteString s
+  = "'" ++ concatMap escapeChar s ++ "'"
+  where
+    escapeChar a = if isBadChar a
+      then "\\x" ++ (showHex (ord a) "") ++ "\\"
+      else [a]
+    isBadChar a = case ord a of
+      x | x <= 31 -> True
+      _ | a == '\'' -> True
+      _ | a == '\\' -> True
+      x | x >= 127 -> True
+      _ -> False