src/Pure/Isar/code.ML

 
 structure Code : PRIVATE_CODE =
 struct
 
 (** auxiliary **)
-
-(* close theorem for storage *)
-
-val close = Thm.trim_context o Thm.close_derivation;
-
 
 (* printing *)
 
 fun string_of_typ thy =
   Syntax.string_of_typ (Config.put show_sorts true (Syntax.init_pretty_global thy));

       cert
   | constrain_cert thy sorts (Abstract (abs_thm, tyco)) =
       Abstract (snd (constrain_thm thy (fst (typscheme_abs thy abs_thm)) sorts abs_thm), tyco);
 
 fun conclude_cert (Nothing cert_thm) =
-      Nothing (Thm.close_derivation cert_thm)
+      Nothing (Thm.close_derivation \<^here> cert_thm)
   | conclude_cert (Equations (cert_thm, propers)) =
-      Equations (Thm.close_derivation cert_thm, propers)
+      Equations (Thm.close_derivation \<^here> cert_thm, propers)
   | conclude_cert (cert as Projection _) =
       cert
   | conclude_cert (Abstract (abs_thm, tyco)) =
-      Abstract (Thm.close_derivation abs_thm, tyco);
+      Abstract (Thm.close_derivation \<^here> abs_thm, tyco);
 
 fun typscheme_of_cert thy (Nothing cert_thm) =
       fst (get_head thy cert_thm)
   | typscheme_of_cert thy (Equations (cert_thm, _)) =
       fst (get_head thy cert_thm)

     fun drop (thm', proper') = if (proper orelse not proper')
       andalso matches_args (args_of thm') then
         (if verbose then warning ("Code generator: dropping subsumed code equation\n" ^
             Thm.string_of_thm_global thy thm') else (); true)
       else false;
-  in (close thm, proper) :: filter_out drop eqns end;
+  in (thm |> Thm.close_derivation \<^here> |> Thm.trim_context, proper) :: filter_out drop eqns end;
 
 fun add_eqn_for (c, eqn) thy =
   thy |> modify_specs (modify_pending_eqns c (subsumptive_add thy true eqn));
 
 fun add_eqns_for default (c, proto_eqns) thy =

           |> fold_rev (subsumptive_add thy (not default)) proto_eqns;
       in specs |> register_fun_spec c (Eqns (default, eqns)) end
     else specs);
 
 fun add_abstract_for (c, (thm, tyco_abs as (tyco, _))) =
-  modify_specs (register_fun_spec c (Abstr (Thm.close_derivation thm, tyco_abs))
+  modify_specs (register_fun_spec c (Abstr (Thm.close_derivation \<^here> thm, tyco_abs))
     #> map_types (History.modify_entry tyco (add_abstract_function c)))
 
 in
 
 fun generic_declare_eqns default strictness raw_eqns thy =