src/Tools/code/code_thingol.ML

   | _ => [];
 
 
 (** translation kernel **)
 
-type transaction = Graph.key option * program;
-
 fun ensure_stmt stmtgen name (dep, program) =
   let
     val add_dep = case dep of NONE => I | SOME dep => Graph.add_edge (dep, name);
     fun add_stmt false =
           Graph.default_node (name, NoStmt)

       fold_map (fn superclass => ensure_class thy algbr funcgr superclass
         ##>> ensure_classrel thy algbr funcgr (class, superclass)) superclasses
       ##>> fold_map (fn (c, ty) => ensure_const thy algbr funcgr c
         ##>> exprgen_typ thy algbr funcgr ty) cs
       #>> (fn info => Class (unprefix "'" Name.aT, info))
-  in
-    ensure_stmt stmt_class class'
-  end
+  in ensure_stmt stmt_class class' end
 and ensure_classrel thy algbr funcgr (subclass, superclass) =
   let
     val classrel' = CodeName.classrel thy (subclass, superclass);
     val stmt_classrel =
       ensure_class thy algbr funcgr subclass
       ##>> ensure_class thy algbr funcgr superclass
       #>> Classrel;
-  in
-    ensure_stmt stmt_classrel classrel'
-  end
+  in ensure_stmt stmt_classrel classrel' end
 and ensure_tyco thy algbr funcgr "fun" =
       pair "fun"
   | ensure_tyco thy algbr funcgr tyco =
       let
         val stmt_datatype =

               ensure_const thy algbr funcgr c
               ##>> fold_map (exprgen_typ thy algbr funcgr) tys) cos
             #>> Datatype
           end;
         val tyco' = CodeName.tyco thy tyco;
-      in
-        ensure_stmt stmt_datatype tyco'
-      end
+      in ensure_stmt stmt_datatype tyco' end
 and exprgen_tyvar_sort thy (algbr as (proj_sort, _)) funcgr (v, sort) =
   fold_map (ensure_class thy algbr funcgr) (proj_sort sort)
   #>> (fn sort => (unprefix "'" v, sort))
-and exprgen_typ thy algbr funcgr (TFree vs) =
-      exprgen_tyvar_sort thy algbr funcgr vs
+and exprgen_typ thy algbr funcgr (TFree v_sort) =
+      exprgen_tyvar_sort thy algbr funcgr v_sort
       #>> (fn (v, sort) => ITyVar v)
   | exprgen_typ thy algbr funcgr (Type (tyco, tys)) =
       ensure_tyco thy algbr funcgr tyco
       ##>> fold_map (exprgen_typ thy algbr funcgr) tys
       #>> (fn (tyco, tys) => tyco `%% tys)

           ##>> (fold_map o fold_map) mk_dict yss
           #>> (fn (inst, dss) => DictConst (inst, dss))
       | mk_dict (Local (classrels, (v, (k, sort)))) =
           fold_map (ensure_classrel thy algbr funcgr) classrels
           #>> (fn classrels => DictVar (classrels, (unprefix "'" v, (k, length sort))))
-  in
-    fold_map mk_dict typargs
-  end
+  in fold_map mk_dict typargs end
 and exprgen_eq thy algbr funcgr thm =
   let
     val (args, rhs) = (apfst (snd o strip_comb) o Logic.dest_equals
       o Logic.unvarify o prop_of) thm;
   in

       ##>> fold_map exprgen_superarity superclasses
       ##>> fold_map exprgen_classparam_inst classparams
       #>> (fn ((((class, tyco), arity), superarities), classparams) =>
              Classinst ((class, (tyco, arity)), (superarities, classparams)));
     val inst = CodeName.instance thy (class, tyco);
-  in
-    ensure_stmt stmt_inst inst
-  end
+  in ensure_stmt stmt_inst inst end
 and ensure_const thy algbr funcgr c =
   let
     val c' = CodeName.const thy c;
     fun stmt_datatypecons tyco =
       ensure_tyco thy algbr funcgr tyco

     val stmtgen = case Code.get_datatype_of_constr thy c
      of SOME tyco => stmt_datatypecons tyco
       | NONE => (case AxClass.class_of_param thy c
          of SOME class => stmt_classparam class
           | NONE => stmt_fun)
-  in
-    ensure_stmt stmtgen c'
-  end
+  in ensure_stmt stmtgen c' end
 and exprgen_term thy algbr funcgr thm (Const (c, ty)) =
       exprgen_app thy algbr funcgr thm ((c, ty), [])
   | exprgen_term thy algbr funcgr thm (Free (v, _)) =
       pair (IVar v)
   | exprgen_term thy algbr funcgr thm (Abs (abs as (_, ty, _))) =