src/Tools/Code/code_thingol.ML

       (*see also signature*);
 
 type program = stmt Graph.T;
 
 fun empty_funs program =
-  Graph.fold (fn (name, (Fun (c, ((_, []), _)), _)) => cons c
-               | _ => I) program [];
+  Graph.fold (fn (_, (Fun (c, ((_, []), _)), _)) => cons c | _ => I) program [];
 
 fun map_terms_bottom_up f (t as IConst _) = f t
   | map_terms_bottom_up f (t as IVar _) = f t
   | map_terms_bottom_up f (t1 `$ t2) = f
       (map_terms_bottom_up f t1 `$ map_terms_bottom_up f t2)

     fun add_dep name = case dep of NONE => I
       | SOME dep => Graph.add_edge (dep, name);
     val (name, naming') = case lookup naming thing
      of SOME name => (name, naming)
       | NONE => declare thing naming;
-  in case try (Graph.get_node program) name
-   of SOME stmt => program
-        |> add_dep name
-        |> pair naming'
-        |> pair dep
-        |> pair name
-    | NONE => program
-        |> Graph.default_node (name, NoStmt)
-        |> add_dep name
-        |> pair naming'
-        |> curry generate (SOME name)
-        ||> snd
-        |-> (fn stmt => (apsnd o Graph.map_node name) (K stmt))
-        |> pair dep
-        |> pair name
+  in
+    if can (Graph.get_node program) name
+    then
+      program
+      |> add_dep name
+      |> pair naming'
+      |> pair dep
+      |> pair name
+    else
+      program
+      |> Graph.default_node (name, NoStmt)
+      |> add_dep name
+      |> pair naming'
+      |> curry generate (SOME name)
+      ||> snd
+      |-> (fn stmt => (apsnd o Graph.map_node name) (K stmt))
+      |> pair dep
+      |> pair name
   end;
 
 exception PERMISSIVE of unit;
 
 fun translation_error thy permissive some_thm msg sub_msg =

 val untag_term = map_types (snd o dest_tagged_type);
 
 fun tag_term (proj_sort, _) eqngr =
   let
     val has_sort_constraints = exists (not o null) o map proj_sort o Code_Preproc.sortargs eqngr;
-    fun tag (Const (c', T')) (Const (c, T)) =
+    fun tag (Const (_, T')) (Const (c, T)) =
         Const (c,
           mk_tagged_type (not (null (Term.add_tvarsT T' [])) andalso has_sort_constraints c, T))
       | tag (t1 $ u1) (t $ u) = tag t1 t $ tag u1 u
       | tag (Abs (_, _, t1)) (Abs (x, T, t)) = Abs (x, T, tag t1 t)
       | tag (Free _) (t as Free _) = t

 fun dynamic_value thy postproc evaluator =
   Code_Preproc.dynamic_value thy postproc (dynamic_evaluator thy evaluator);
 
 fun lift_evaluation thy evaluation' algebra eqngr naming program vs t =
   let
-    val (((_, program'), (((vs', ty'), t'), deps)), _) =
+    val (((_, _), (((vs', ty'), t'), deps)), _) =
       ensure_value thy algebra eqngr t (NONE, (naming, program));
   in evaluation' ((original_sorts vs vs', (vs', ty')), t') deps end;
 
 fun lift_evaluator thy evaluator' consts algebra eqngr =
   let

 
 fun lift_evaluator_simple thy evaluator' consts algebra eqngr =
   let
     fun generate_consts thy algebra eqngr =
       fold_map (ensure_const thy algebra eqngr false);
-    val (consts', (naming, program)) =
+    val (_, (_, program)) =
       invoke_generation true thy (algebra, eqngr) generate_consts consts;
   in evaluator' program end;
 
 fun static_conv thy consts conv =
   Code_Preproc.static_conv thy consts (lift_evaluator thy conv consts);