# HG changeset patch
# User wenzelm
# Date 1436116120 -7200
# Node ID 441e268564c7ec6ed3a7ad042f86c9f4617eefed
# Parent  2affe7e97a345880f0bf320d261933efad09c253
clarified context;

diff -r 2affe7e97a34 -r 441e268564c7 src/FOLP/ex/Nat.thy
--- a/src/FOLP/ex/Nat.thy	Sun Jul 05 16:44:59 2015 +0200
+++ b/src/FOLP/ex/Nat.thy	Sun Jul 05 19:08:40 2015 +0200
@@ -89,19 +89,19 @@
 
 schematic_lemma add_assoc: "?p : (k+m)+n = k+(m+n)"
 apply (rule_tac n = k in induct)
-apply (tactic {* SIMP_TAC add_ss 1 *})
-apply (tactic {* ASM_SIMP_TAC add_ss 1 *})
+apply (tactic {* SIMP_TAC @{context} add_ss 1 *})
+apply (tactic {* ASM_SIMP_TAC @{context} add_ss 1 *})
 done
 
 schematic_lemma add_0_right: "?p : m+0 = m"
 apply (rule_tac n = m in induct)
-apply (tactic {* SIMP_TAC add_ss 1 *})
-apply (tactic {* ASM_SIMP_TAC add_ss 1 *})
+apply (tactic {* SIMP_TAC @{context} add_ss 1 *})
+apply (tactic {* ASM_SIMP_TAC @{context} add_ss 1 *})
 done
 
 schematic_lemma add_Suc_right: "?p : m+Suc(n) = Suc(m+n)"
 apply (rule_tac n = m in induct)
-apply (tactic {* ALLGOALS (ASM_SIMP_TAC add_ss) *})
+apply (tactic {* ALLGOALS (ASM_SIMP_TAC @{context} add_ss) *})
 done
 
 (*mk_typed_congs appears not to work with FOLP's version of subst*)
diff -r 2affe7e97a34 -r 441e268564c7 src/FOLP/simp.ML
--- a/src/FOLP/simp.ML	Sun Jul 05 16:44:59 2015 +0200
+++ b/src/FOLP/simp.ML	Sun Jul 05 19:08:40 2015 +0200
@@ -37,13 +37,13 @@
   val dest_ss   : simpset -> thm list * thm list
   val print_ss  : Proof.context -> simpset -> unit
   val setauto   : simpset * (int -> tactic) -> simpset
-  val ASM_SIMP_CASE_TAC : simpset -> int -> tactic
-  val ASM_SIMP_TAC      : simpset -> int -> tactic
+  val ASM_SIMP_CASE_TAC : Proof.context -> simpset -> int -> tactic
+  val ASM_SIMP_TAC      : Proof.context -> simpset -> int -> tactic
   val CASE_TAC          : simpset -> int -> tactic
-  val SIMP_CASE2_TAC    : simpset -> int -> tactic
-  val SIMP_THM          : simpset -> thm -> thm
-  val SIMP_TAC          : simpset -> int -> tactic
-  val SIMP_CASE_TAC     : simpset -> int -> tactic
+  val SIMP_CASE2_TAC    : Proof.context -> simpset -> int -> tactic
+  val SIMP_THM          : Proof.context -> simpset -> thm -> thm
+  val SIMP_TAC          : Proof.context -> simpset -> int -> tactic
+  val SIMP_CASE_TAC     : Proof.context -> simpset -> int -> tactic
   val mk_congs          : theory -> string list -> thm list
   val mk_typed_congs    : theory -> (string * string) list -> thm list
 (* temporarily disabled:
@@ -375,26 +375,25 @@
     in variants_abs (params, Logic.strip_assums_concl subgi) end;
 
 (*print lhs of conclusion of subgoal i*)
-fun pr_goal_lhs i st =
-    writeln (Syntax.string_of_term_global (Thm.theory_of_thm st)
-             (lhs_of (prepare_goal i st)));
+fun pr_goal_lhs ctxt i st =
+    writeln (Syntax.string_of_term ctxt (lhs_of (prepare_goal i st)));
 
 (*print conclusion of subgoal i*)
-fun pr_goal_concl i st =
-    writeln (Syntax.string_of_term_global (Thm.theory_of_thm st) (prepare_goal i st))
+fun pr_goal_concl ctxt i st =
+    writeln (Syntax.string_of_term ctxt (prepare_goal i st))
 
 (*print subgoals i to j (inclusive)*)
-fun pr_goals (i,j) st =
+fun pr_goals ctxt (i,j) st =
     if i>j then ()
-    else (pr_goal_concl i st;  pr_goals (i+1,j) st);
+    else (pr_goal_concl ctxt i st;  pr_goals ctxt (i+1,j) st);
 
 (*Print rewrite for tracing; i=subgoal#, n=number of new subgoals,
   thm=old state, thm'=new state *)
-fun pr_rew (i,n,thm,thm',not_asms) =
+fun pr_rew ctxt (i,n,thm,thm',not_asms) =
     if !tracing
     then (if not_asms then () else writeln"Assumption used in";
-          pr_goal_lhs i thm; writeln"->"; pr_goal_lhs (i+n) thm';
-          if n>0 then (writeln"Conditions:"; pr_goals (i, i+n-1) thm')
+          pr_goal_lhs ctxt i thm; writeln"->"; pr_goal_lhs ctxt (i+n) thm';
+          if n>0 then (writeln"Conditions:"; pr_goals ctxt (i, i+n-1) thm')
           else ();
           writeln"" )
     else ();
@@ -407,7 +406,8 @@
         strip_varify(t,n,Var(("?",length vs),T)::vs)
   | strip_varify  _  = [];
 
-fun execute(ss,if_fl,auto_tac,cong_tac,net,i,thm) = let
+fun execute ctxt (ss,if_fl,auto_tac,cong_tac,net,i,thm) =
+let
 
 fun simp_lhs(thm,ss,anet,ats,cs) =
     if var_lhs(thm,i) then (ss,thm,anet,ats,cs) else
@@ -426,7 +426,7 @@
       are represented by rules, generalized over their parameters*)
 fun add_asms(ss,thm,a,anet,ats,cs) =
     let val As = strip_varify(nth_subgoal i thm, a, []);
-        val thms = map (Thm.trivial o Thm.global_cterm_of(Thm.theory_of_thm thm)) As;
+        val thms = map (Thm.trivial o Thm.cterm_of ctxt) As;
         val new_rws = maps mk_rew_rules thms;
         val rwrls = map mk_trans (maps mk_rew_rules thms);
         val anet' = fold_rev lhs_insert_thm rwrls anet;
@@ -435,7 +435,7 @@
 fun rew(seq,thm,ss,anet,ats,cs, more) = case Seq.pull seq of
       SOME(thm',seq') =>
             let val n = (Thm.nprems_of thm') - (Thm.nprems_of thm)
-            in pr_rew(i,n,thm,thm',more);
+            in pr_rew ctxt (i,n,thm,thm',more);
                if n=0 then (SIMP_LHS::ss, thm', anet, ats, cs)
                else ((replicate n PROVE) @ (POP_CS::SIMP_LHS::ss),
                      thm', anet, ats, (ss,thm,anet,ats,seq',more)::cs)
@@ -451,7 +451,7 @@
     | NONE => let val (ss0,thm0,anet0,ats0,seq,more)::cs0 = cs
               in if !tracing
                  then (writeln"*** Failed to prove precondition. Normal form:";
-                       pr_goal_concl i thm;  writeln"")
+                       pr_goal_concl ctxt i thm;  writeln"")
                  else ();
                  rew(seq,thm0,ss0,anet0,ats0,cs0,more)
               end;
@@ -480,30 +480,30 @@
 in exec(ss, thm, Net.empty, [], []) end;
 
 
-fun EXEC_TAC(ss,fl) (SS{auto_tac,cong_net,simp_net,...}) =
+fun EXEC_TAC ctxt (ss,fl) (SS{auto_tac,cong_net,simp_net,...}) =
 let val cong_tac = net_tac cong_net
 in fn i =>
     (fn thm =>
      if i <= 0 orelse Thm.nprems_of thm < i then Seq.empty
-     else Seq.single(execute(ss,fl,auto_tac,cong_tac,simp_net,i,thm)))
+     else Seq.single(execute ctxt (ss,fl,auto_tac,cong_tac,simp_net,i,thm)))
     THEN TRY(auto_tac i)
 end;
 
-val SIMP_TAC = EXEC_TAC([MK_EQ,SIMP_LHS,REFL,STOP],false);
-val SIMP_CASE_TAC = EXEC_TAC([MK_EQ,SIMP_LHS,IF,REFL,STOP],false);
+fun SIMP_TAC ctxt = EXEC_TAC ctxt ([MK_EQ,SIMP_LHS,REFL,STOP],false);
+fun SIMP_CASE_TAC ctxt = EXEC_TAC ctxt ([MK_EQ,SIMP_LHS,IF,REFL,STOP],false);
 
-val ASM_SIMP_TAC = EXEC_TAC([ASMS(0),MK_EQ,SIMP_LHS,REFL,STOP],false);
-val ASM_SIMP_CASE_TAC = EXEC_TAC([ASMS(0),MK_EQ,SIMP_LHS,IF,REFL,STOP],false);
+fun ASM_SIMP_TAC ctxt = EXEC_TAC ctxt ([ASMS(0),MK_EQ,SIMP_LHS,REFL,STOP],false);
+fun ASM_SIMP_CASE_TAC ctxt = EXEC_TAC ctxt ([ASMS(0),MK_EQ,SIMP_LHS,IF,REFL,STOP],false);
 
-val SIMP_CASE2_TAC = EXEC_TAC([MK_EQ,SIMP_LHS,IF,REFL,STOP],true);
+fun SIMP_CASE2_TAC ctxt = EXEC_TAC ctxt ([MK_EQ,SIMP_LHS,IF,REFL,STOP],true);
 
-fun REWRITE (ss,fl) (SS{auto_tac,cong_net,simp_net,...}) =
+fun REWRITE ctxt (ss,fl) (SS{auto_tac,cong_net,simp_net,...}) =
 let val cong_tac = net_tac cong_net
 in fn thm => let val state = thm RSN (2,red1)
-             in execute(ss,fl,auto_tac,cong_tac,simp_net,1,state) end
+             in execute ctxt (ss,fl,auto_tac,cong_tac,simp_net,1,state) end
 end;
 
-val SIMP_THM = REWRITE ([ASMS(0),SIMP_LHS,IF,REFL,STOP],false);
+fun SIMP_THM ctxt = REWRITE ctxt ([ASMS(0),SIMP_LHS,IF,REFL,STOP],false);
 
 
 (* Compute Congruence rules for individual constants using the substition