# HG changeset patch
# User haftmann
# Date 1172216367 -3600
# Node ID ec6a033b27be1a2e96903a2840c70550f67e0c71
# Parent  c818c6b836f51a53273ab0125d82c8990fb027ec
proper treatment of -> as type constructor

diff -r c818c6b836f5 -r ec6a033b27be src/Pure/Tools/codegen_package.ML
--- a/src/Pure/Tools/codegen_package.ML	Fri Feb 23 08:39:26 2007 +0100
+++ b/src/Pure/Tools/codegen_package.ML	Fri Feb 23 08:39:27 2007 +0100
@@ -141,31 +141,34 @@
 and ensure_def_classrel thy algbr funcgr strct (subclass, superclass) =
   ensure_def_class thy algbr funcgr strct subclass
   #>> (fn _ => CodegenNames.classrel thy (subclass, superclass))
-and ensure_def_tyco thy algbr funcgr strct tyco trns =
-  let
-    fun defgen_datatype trns =
-      case CodegenData.get_datatype thy tyco
-       of SOME (vs, cos) =>
-            trns
-            |> fold_map (exprgen_tyvar_sort thy algbr funcgr strct) vs
-            ||>> fold_map (fn (c, tys) =>
-              fold_map (exprgen_type thy algbr funcgr strct) tys
-              #-> (fn tys' =>
-                pair ((CodegenNames.const thy o CodegenConsts.norm_of_typ thy)
-                  (c, tys ---> Type (tyco, map TFree vs)), tys'))) cos
-            |-> (fn (vs, cos) => succeed (CodegenThingol.Datatype (vs, cos)))
-        | NONE =>
-            trns
-            |> fail ("No such datatype: " ^ quote tyco)
-    val tyco' = CodegenNames.tyco thy tyco;
-    val strict = check_strict strct (CodegenSerializer.tyco_has_serialization thy) tyco';
-  in
-    trns
-    |> tracing (fn _ => "generating type constructor " ^ quote tyco)
-    |> ensure_def thy defgen_datatype strict
-        ("generating type constructor " ^ quote tyco) tyco'
-    |> pair tyco'
-  end
+and ensure_def_tyco thy algbr funcgr strct "fun" trns =
+      trns
+      |> pair "fun"
+  | ensure_def_tyco thy algbr funcgr strct tyco trns =
+      let
+        fun defgen_datatype trns =
+          case CodegenData.get_datatype thy tyco
+           of SOME (vs, cos) =>
+                trns
+                |> fold_map (exprgen_tyvar_sort thy algbr funcgr strct) vs
+                ||>> fold_map (fn (c, tys) =>
+                  fold_map (exprgen_type thy algbr funcgr strct) tys
+                  #-> (fn tys' =>
+                    pair ((CodegenNames.const thy o CodegenConsts.norm_of_typ thy)
+                      (c, tys ---> Type (tyco, map TFree vs)), tys'))) cos
+                |-> (fn (vs, cos) => succeed (CodegenThingol.Datatype (vs, cos)))
+            | NONE =>
+                trns
+                |> fail ("No such datatype: " ^ quote tyco)
+        val tyco' = CodegenNames.tyco thy tyco;
+        val strict = check_strict strct (CodegenSerializer.tyco_has_serialization thy) tyco';
+      in
+        trns
+        |> tracing (fn _ => "generating type constructor " ^ quote tyco)
+        |> ensure_def thy defgen_datatype strict
+            ("generating type constructor " ^ quote tyco) tyco'
+        |> pair tyco'
+      end
 and exprgen_tyvar_sort thy (algbr as ((proj_sort, _), _)) funcgr strct (v, sort) trns =
   trns
   |> fold_map (ensure_def_class thy algbr funcgr strct) (proj_sort sort)
@@ -174,11 +177,6 @@
       trns
       |> exprgen_tyvar_sort thy algbr funcgr strct vs
       |>> (fn (v, sort) => ITyVar v)
-  | exprgen_type thy algbr funcgr strct (Type ("fun", [t1, t2])) trns =
-      trns
-      |> exprgen_type thy algbr funcgr strct t1
-      ||>> exprgen_type thy algbr funcgr strct t2
-      |>> (fn (t1', t2') => t1' `-> t2')
   | exprgen_type thy algbr funcgr strct (Type (tyco, tys)) trns =
       case get_abstype thy (tyco, tys)
        of SOME ty =>