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, _)) =