1.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml	Thu Jul 28 11:43:27 2022 +0200
     1.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml	Sat Jul 30 16:47:45 2022 +0200
     1.3 @@ -81,8 +81,8 @@
     1.4    val is_rewtac : input -> bool
     1.5    val is_rewset : input -> bool
     1.6    val rls_of : input -> Rule_Set.id
     1.7 -  val rule2tac : theory -> Env.T ->  Rule.rule -> input
     1.8 -  val applicable : theory -> string -> Rule_Set.T -> term -> input ->input list
     1.9 +  val rule2tac : Proof.context -> Env.T ->  Rule.rule -> input
    1.10 +  val applicable : Proof.context -> string -> Rule_Set.T -> term -> input ->input list
    1.11    val for_specify: input -> bool
    1.12  
    1.13    val input_from_T : T -> input
    1.14 @@ -228,7 +228,7 @@
    1.15    | rls_of (Rewrite_Set rls) = rls
    1.16    | rls_of input = raise ERROR ("rls_of: called with input \"" ^ tac2IDstr input ^ "\"");
    1.17  
    1.18 -fun rule2tac thy _ (Rule.Eval (opID, _)) = Calculate (assoc_calc thy opID)
    1.19 +fun rule2tac ctxt _ (Rule.Eval (opID, _)) = Calculate (assoc_calc (Proof_Context.theory_of ctxt) opID)
    1.20    | rule2tac _ [] (Rule.Thm thm'') = Rewrite thm''
    1.21    | rule2tac _ subst (Rule.Thm thm'') = 
    1.22      Rewrite_Inst (Subst.T_to_input subst, thm'')
    1.23 @@ -240,21 +240,21 @@
    1.24  
    1.25  (* try if a rewrite-rule is applicable to a given formula; 
    1.26     in case of rule-sets (recursivley) collect all _atomic_ rewrites *) 
    1.27 -fun try_rew thy ((_, ro) : Rewrite_Ord.rew_ord) erls (subst : subst) f (thm' as Rule.Thm (_, thm)) =
    1.28 +fun try_rew ctxt ((_, ro) : Rewrite_Ord.rew_ord) erls (subst : subst) f (thm' as Rule.Thm (_, thm)) =
    1.29      if Auto_Prog.contains_bdv thm
    1.30 -    then case Rewrite.rewrite_inst_ thy ro erls false subst thm f of
    1.31 -	    SOME _ => [rule2tac thy subst thm']
    1.32 +    then case Rewrite.rewrite_inst_ ctxt ro erls false subst thm f of
    1.33 +	    SOME _ => [rule2tac ctxt subst thm']
    1.34  	  | NONE => []
    1.35 -    else (case Rewrite.rewrite_ thy ro erls false thm f of
    1.36 -	    SOME _ => [rule2tac thy [] thm']
    1.37 +    else (case Rewrite.rewrite_ ctxt ro erls false thm f of
    1.38 +	    SOME _ => [rule2tac ctxt [] thm']
    1.39  	  | NONE => [])
    1.40 -  | try_rew thy _ _ _ f (cal as Rule.Eval c) = 
    1.41 -    (case Eval.adhoc_thm thy c f of
    1.42 -	    SOME _ => [rule2tac thy [] cal]
    1.43 +  | try_rew ctxt _ _ _ f (cal as Rule.Eval c) = 
    1.44 +    (case Eval.adhoc_thm (Proof_Context.theory_of ctxt) c f of
    1.45 +	    SOME _ => [rule2tac ctxt [] cal]
    1.46      | NONE => [])
    1.47 -  | try_rew thy _ _ _ f (cal as Rule.Cal1 c) = 
    1.48 -    (case Eval.adhoc_thm thy c f of
    1.49 -	      SOME _ => [rule2tac thy [] cal]
    1.50 +  | try_rew ctxt _ _ _ f (cal as Rule.Cal1 c) = 
    1.51 +    (case Eval.adhoc_thm (Proof_Context.theory_of ctxt) c f of
    1.52 +	      SOME _ => [rule2tac ctxt [] cal]
    1.53        | NONE => [])
    1.54    | try_rew thy _ _ subst f (Rule.Rls_ rls) = filter_appl_rews thy subst f rls
    1.55    | try_rew _ _ _ _ _ _ = raise ERROR "try_rew: uncovered case"
    1.56 @@ -267,12 +267,13 @@
    1.57  
    1.58  (* decide if a tactic is applicable to a given formula; 
    1.59     in case of Rewrite_Set* go down to _atomic_ rewrite-tactics *)
    1.60 -fun applicable thy _ _ f (Calculate scrID) =
    1.61 -    try_rew thy Rewrite_Ord.e_rew_ordX Rule_Set.empty [] f (Rule.Eval (assoc_calc' thy scrID |> snd))
    1.62 -  | applicable thy ro erls f (Rewrite thm'') =
    1.63 -    try_rew thy (ro, Rewrite_Ord.assoc_rew_ord ro) erls [] f (Rule.Thm thm'')
    1.64 -  | applicable thy ro erls f (Rewrite_Inst (subs, thm'')) =
    1.65 -    try_rew thy (ro, Rewrite_Ord.assoc_rew_ord ro) erls (Subst.T_from_input thy subs) f (Rule.Thm thm'')
    1.66 +fun applicable ctxt _ _ f (Calculate scrID) =
    1.67 +    try_rew ctxt Rewrite_Ord.e_rew_ordX Rule_Set.empty [] f 
    1.68 +      (Rule.Eval (assoc_calc' (Proof_Context.theory_of ctxt) scrID |> snd))
    1.69 +  | applicable ctxt ro erls f (Rewrite thm'') =
    1.70 +    try_rew ctxt (ro, Rewrite_Ord.assoc_rew_ord ro) erls [] f (Rule.Thm thm'')
    1.71 +  | applicable ctxt ro erls f (Rewrite_Inst (subs, thm'')) =
    1.72 +    try_rew ctxt (ro, Rewrite_Ord.assoc_rew_ord ro) erls (Subst.T_from_input ctxt subs) f (Rule.Thm thm'')
    1.73  
    1.74    | applicable thy _ _ f (Rewrite_Set rls') =
    1.75      filter_appl_rews thy [] f (assoc_rls rls')