1.1 --- a/src/Tools/code/code_thingol.ML Tue Jul 01 07:58:17 2008 +0200
1.2 +++ b/src/Tools/code/code_thingol.ML Tue Jul 01 07:58:37 2008 +0200
1.3 @@ -298,8 +298,6 @@
1.4
1.5 (** translation kernel **)
1.6
1.7 -type transaction = Graph.key option * program;
1.8 -
1.9 fun ensure_stmt stmtgen name (dep, program) =
1.10 let
1.11 val add_dep = case dep of NONE => I | SOME dep => Graph.add_edge (dep, name);
1.12 @@ -338,9 +336,7 @@
1.13 ##>> fold_map (fn (c, ty) => ensure_const thy algbr funcgr c
1.14 ##>> exprgen_typ thy algbr funcgr ty) cs
1.15 #>> (fn info => Class (unprefix "'" Name.aT, info))
1.16 - in
1.17 - ensure_stmt stmt_class class'
1.18 - end
1.19 + in ensure_stmt stmt_class class' end
1.20 and ensure_classrel thy algbr funcgr (subclass, superclass) =
1.21 let
1.22 val classrel' = CodeName.classrel thy (subclass, superclass);
1.23 @@ -348,9 +344,7 @@
1.24 ensure_class thy algbr funcgr subclass
1.25 ##>> ensure_class thy algbr funcgr superclass
1.26 #>> Classrel;
1.27 - in
1.28 - ensure_stmt stmt_classrel classrel'
1.29 - end
1.30 + in ensure_stmt stmt_classrel classrel' end
1.31 and ensure_tyco thy algbr funcgr "fun" =
1.32 pair "fun"
1.33 | ensure_tyco thy algbr funcgr tyco =
1.34 @@ -366,14 +360,12 @@
1.35 #>> Datatype
1.36 end;
1.37 val tyco' = CodeName.tyco thy tyco;
1.38 - in
1.39 - ensure_stmt stmt_datatype tyco'
1.40 - end
1.41 + in ensure_stmt stmt_datatype tyco' end
1.42 and exprgen_tyvar_sort thy (algbr as (proj_sort, _)) funcgr (v, sort) =
1.43 fold_map (ensure_class thy algbr funcgr) (proj_sort sort)
1.44 #>> (fn sort => (unprefix "'" v, sort))
1.45 -and exprgen_typ thy algbr funcgr (TFree vs) =
1.46 - exprgen_tyvar_sort thy algbr funcgr vs
1.47 +and exprgen_typ thy algbr funcgr (TFree v_sort) =
1.48 + exprgen_tyvar_sort thy algbr funcgr v_sort
1.49 #>> (fn (v, sort) => ITyVar v)
1.50 | exprgen_typ thy algbr funcgr (Type (tyco, tys)) =
1.51 ensure_tyco thy algbr funcgr tyco
1.52 @@ -406,9 +398,7 @@
1.53 | mk_dict (Local (classrels, (v, (k, sort)))) =
1.54 fold_map (ensure_classrel thy algbr funcgr) classrels
1.55 #>> (fn classrels => DictVar (classrels, (unprefix "'" v, (k, length sort))))
1.56 - in
1.57 - fold_map mk_dict typargs
1.58 - end
1.59 + in fold_map mk_dict typargs end
1.60 and exprgen_eq thy algbr funcgr thm =
1.61 let
1.62 val (args, rhs) = (apfst (snd o strip_comb) o Logic.dest_equals
1.63 @@ -454,9 +444,7 @@
1.64 #>> (fn ((((class, tyco), arity), superarities), classparams) =>
1.65 Classinst ((class, (tyco, arity)), (superarities, classparams)));
1.66 val inst = CodeName.instance thy (class, tyco);
1.67 - in
1.68 - ensure_stmt stmt_inst inst
1.69 - end
1.70 + in ensure_stmt stmt_inst inst end
1.71 and ensure_const thy algbr funcgr c =
1.72 let
1.73 val c' = CodeName.const thy c;
1.74 @@ -486,9 +474,7 @@
1.75 | NONE => (case AxClass.class_of_param thy c
1.76 of SOME class => stmt_classparam class
1.77 | NONE => stmt_fun)
1.78 - in
1.79 - ensure_stmt stmtgen c'
1.80 - end
1.81 + in ensure_stmt stmtgen c' end
1.82 and exprgen_term thy algbr funcgr thm (Const (c, ty)) =
1.83 exprgen_app thy algbr funcgr thm ((c, ty), [])
1.84 | exprgen_term thy algbr funcgr thm (Free (v, _)) =