src/Pure/goal.ML

   val init: cterm -> thm
   val protect: int -> thm -> thm
   val conclude: thm -> thm
   val check_finished: Proof.context -> thm -> thm
   val finish: Proof.context -> thm -> thm
-  val norm_result: thm -> thm
+  val norm_result: Proof.context -> thm -> thm
   val skip_proofs_enabled: unit -> bool
   val future_enabled: int -> bool
   val future_enabled_timing: Time.time -> bool
   val future_result: Proof.context -> thm future -> term -> thm
-  val prove_internal: cterm list -> cterm -> (thm list -> tactic) -> thm
+  val prove_internal: Proof.context -> cterm list -> cterm -> (thm list -> tactic) -> thm
   val is_schematic: term -> bool
   val prove_multi: Proof.context -> string list -> term list -> term list ->
     ({prems: thm list, context: Proof.context} -> tactic) -> thm list
   val prove_future: Proof.context -> string list -> term list -> term ->
     ({prems: thm list, context: Proof.context} -> tactic) -> thm

 
 (** results **)
 
 (* normal form *)
 
-val norm_result =
+fun norm_result ctxt =
   Drule.flexflex_unique
-  #> Raw_Simplifier.norm_hhf_protect
+  #> Raw_Simplifier.norm_hhf_protect ctxt
   #> Thm.strip_shyps
   #> Drule.zero_var_indexes;
 
 
 (* scheduling parameters *)

 
 (** tactical theorem proving **)
 
 (* prove_internal -- minimal checks, no normalization of result! *)
 
-fun prove_internal casms cprop tac =
-  (case SINGLE (tac (map Assumption.assume casms)) (init cprop) of
+fun prove_internal ctxt casms cprop tac =
+  (case SINGLE (tac (map (Assumption.assume ctxt) casms)) (init cprop) of
     SOME th => Drule.implies_intr_list casms
       (finish (Syntax.init_pretty_global (Thm.theory_of_thm th)) th)
   | NONE => error "Tactic failed");
 
 

   let
     val ((_, goal'), ctxt') = Variable.focus_cterm goal ctxt;
     val goal'' = Drule.cterm_rule (singleton (Variable.export ctxt' ctxt)) goal';
     val Rs = filter (non_atomic o Thm.term_of) (Drule.strip_imp_prems goal'');
     val tacs = Rs |> map (fn R =>
-      etac (Raw_Simplifier.norm_hhf (Thm.trivial R)) THEN_ALL_NEW assume_tac);
+      etac (Raw_Simplifier.norm_hhf ctxt (Thm.trivial R)) THEN_ALL_NEW assume_tac);
   in fold_rev (curry op APPEND') tacs (K no_tac) i end);
 
 
 
 (** parallel tacticals **)