# HG changeset patch
# User boehmes
# Date 1267085776 -3600
# Node ID 63fb71d29eba7e791cbbde8fa1603b66d35e6649
# Parent  413f9ba7e30818a1182b4f0937a9efabe32e2732
use mixfix syntax for Boogie types

diff -r 413f9ba7e308 -r 63fb71d29eba src/HOL/Boogie/Tools/boogie_loader.ML
--- a/src/HOL/Boogie/Tools/boogie_loader.ML	Wed Feb 24 22:45:14 2010 +0100
+++ b/src/HOL/Boogie/Tools/boogie_loader.ML	Thu Feb 25 09:16:16 2010 +0100
@@ -49,6 +49,26 @@
   if line = 0 orelse col = 0 then no_label_name
   else label_prefix ^ string_of_int line ^ "_" ^ string_of_int col
 
+local
+  val quote_mixfix =
+    Symbol.explode #> map
+      (fn "_" => "'_"
+        | "(" => "'("
+        | ")" => "')"
+        | "/" => "'/"
+        | s => s) #>
+    implode
+in
+fun mk_syntax name i =
+  let
+    val syn = quote_mixfix name
+    val args = concat (separate ",/ " (replicate i "_"))
+  in
+    if i = 0 then Mixfix (syn, [], 1000)
+    else Mixfix (syn ^ "()'(/" ^ args ^ "')", replicate i 0, 1000)
+  end
+end
+
 
 datatype attribute_value = StringValue of string | TermValue of term
 
@@ -78,8 +98,8 @@
       | NONE =>
           let
             val args = Name.variant_list [] (replicate arity "'")
-            val (T, thy') =
-              ObjectLogic.typedecl (Binding.name isa_name, args, NoSyn) thy
+            val (T, thy') = ObjectLogic.typedecl (Binding.name isa_name, args,
+              mk_syntax name arity) thy
             val type_name = fst (Term.dest_Type T)
           in (((name, type_name), log_new name type_name), thy') end)
     end
@@ -93,24 +113,6 @@
 
 
 local
-  val quote_mixfix =
-    Symbol.explode #> map
-      (fn "_" => "'_"
-        | "(" => "'("
-        | ")" => "')"
-        | "/" => "'/"
-        | s => s) #>
-    implode
-
-  fun mk_syntax name i =
-    let
-      val syn = quote_mixfix name
-      val args = concat (separate ",/ " (replicate i "_"))
-    in
-      if i = 0 then Mixfix (syn, [], 1000)
-      else Mixfix (syn ^ "()'(/" ^ args ^ "')", replicate i 0, 1000)
-    end
-
   fun maybe_builtin T =
     let
       fun const name = SOME (Const (name, T))