# HG changeset patch
# User wenzelm
# Date 1004990189 -3600
# Node ID 7e2e84e503ce05589e81dde0c963f5911fae9c67
# Parent  2b8550bb4acdcf23b3f38667f333a845a69905e4
Method.trace ctxt;

diff -r 2b8550bb4acd -r 7e2e84e503ce src/Provers/classical.ML
--- a/src/Provers/classical.ML	Mon Nov 05 20:56:00 2001 +0100
+++ b/src/Provers/classical.ML	Mon Nov 05 20:56:29 2001 +0100
@@ -1094,7 +1094,7 @@
   let fun rules_of (inet, _) = order_rules (Net.unify_term inet concl)
   in flat (map rules_of nets) end;
 
-fun some_rule_tac cs facts =
+fun some_rule_tac ctxt cs facts =
   let
     val nets = get_nets cs;
     val erules = find_erules facts nets;
@@ -1104,11 +1104,14 @@
         val irules = find_rules (Logic.strip_assums_concl goal) nets;
         val rules = erules @ irules;
         val ruleq = Method.multi_resolves facts rules;
-      in Method.trace rules; fn st => Seq.flat (Seq.map (fn rule => Tactic.rtac rule i st) ruleq) end);
+      in
+        Method.trace ctxt rules;
+        fn st => Seq.flat (Seq.map (fn rule => Tactic.rtac rule i st) ruleq)
+      end);
   in tac end;
 
 fun rule_tac [] ctxt cs facts =
-    Method.some_rule_tac [] ctxt facts APPEND' some_rule_tac cs facts
+    Method.some_rule_tac [] ctxt facts APPEND' some_rule_tac ctxt cs facts
   | rule_tac rules _ _ facts = Method.rule_tac rules facts;
 
 fun default_tac rules ctxt cs facts =
diff -r 2b8550bb4acd -r 7e2e84e503ce src/Provers/induct_method.ML
--- a/src/Provers/induct_method.ML	Mon Nov 05 20:56:00 2001 +0100
+++ b/src/Provers/induct_method.ML	Mon Nov 05 20:56:29 2001 +0100
@@ -106,7 +106,7 @@
       | (_, _, None) =>
           let val rules = find_casesS ctxt facts @ find_casesT ctxt insts in
             if null rules then error "Unable to figure out cases rule" else ();
-            Method.trace rules;
+            Method.trace ctxt rules;
             Seq.flat (Seq.map (Seq.try inst_rule) (Seq.of_list rules))
           end
       | (_, _, Some r) => Seq.single (inst_rule r));
@@ -263,7 +263,7 @@
         None =>
           let val rules = find_inductS ctxt facts @ find_inductT ctxt insts in
             if null rules then error "Unable to figure out induct rule" else ();
-            Method.trace rules;
+            Method.trace ctxt rules;
             Seq.flat (Seq.map (Seq.try inst_rule) (Seq.of_list rules))
           end
       | Some r => Seq.single (inst_rule r));