# HG changeset patch
# User blanchet
# Date 1304267844 -7200
# Node ID 77d9915e6a114e04b8e583db0162d908b30eb2b2
# Parent  f6ba908b8b27025350c838dd2ee4e249049df4fe
use postfix syntax for mangled types, for consistency with unmangled

diff -r f6ba908b8b27 -r 77d9915e6a11 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 01 18:37:24 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 01 18:37:24 2011 +0200
@@ -440,7 +440,7 @@
     f name (* FIXME: shouldn't happen *)
     (* raise Fail "impossible schematic type variable" *)
   | mangled_combtyp_component f (CombType (name, tys)) =
-    "(" ^ commas (map (mangled_combtyp_component f) tys) ^ ")" ^ f name
+    f name ^ "(" ^ commas (map (mangled_combtyp_component f) tys) ^ ")"
 
 fun mangled_combtyp ty =
   (make_type (mangled_combtyp_component fst ty),
@@ -459,9 +459,9 @@
   Scan.many1 (not o member (op =) ["(", ")", ","]) >> implode
 
 fun parse_mangled_type x =
-  ($$ "(" |-- Scan.optional parse_mangled_types [] --| $$ ")"
-      -- parse_mangled_ident >> (ATerm o swap)
-   || parse_mangled_ident >> (ATerm o rpair [])) x
+  (parse_mangled_ident
+   -- Scan.optional ($$ "(" |-- Scan.optional parse_mangled_types [] --| $$ ")")
+                    [] >> ATerm) x
 and parse_mangled_types x =
   (parse_mangled_type ::: Scan.repeat ($$ "," |-- parse_mangled_type)) x