Method.trace ctxt;
authorwenzelm
Mon Nov 05 20:56:29 2001 +0100 (2001-11-05 ago)
changeset 120537e2e84e503ce
parent 12052 2b8550bb4acd
child 12054 a96c9563d568
Method.trace ctxt;
src/Provers/classical.ML
src/Provers/induct_method.ML
     1.1 --- a/src/Provers/classical.ML	Mon Nov 05 20:56:00 2001 +0100
     1.2 +++ b/src/Provers/classical.ML	Mon Nov 05 20:56:29 2001 +0100
     1.3 @@ -1094,7 +1094,7 @@
     1.4    let fun rules_of (inet, _) = order_rules (Net.unify_term inet concl)
     1.5    in flat (map rules_of nets) end;
     1.6  
     1.7 -fun some_rule_tac cs facts =
     1.8 +fun some_rule_tac ctxt cs facts =
     1.9    let
    1.10      val nets = get_nets cs;
    1.11      val erules = find_erules facts nets;
    1.12 @@ -1104,11 +1104,14 @@
    1.13          val irules = find_rules (Logic.strip_assums_concl goal) nets;
    1.14          val rules = erules @ irules;
    1.15          val ruleq = Method.multi_resolves facts rules;
    1.16 -      in Method.trace rules; fn st => Seq.flat (Seq.map (fn rule => Tactic.rtac rule i st) ruleq) end);
    1.17 +      in
    1.18 +        Method.trace ctxt rules;
    1.19 +        fn st => Seq.flat (Seq.map (fn rule => Tactic.rtac rule i st) ruleq)
    1.20 +      end);
    1.21    in tac end;
    1.22  
    1.23  fun rule_tac [] ctxt cs facts =
    1.24 -    Method.some_rule_tac [] ctxt facts APPEND' some_rule_tac cs facts
    1.25 +    Method.some_rule_tac [] ctxt facts APPEND' some_rule_tac ctxt cs facts
    1.26    | rule_tac rules _ _ facts = Method.rule_tac rules facts;
    1.27  
    1.28  fun default_tac rules ctxt cs facts =
     2.1 --- a/src/Provers/induct_method.ML	Mon Nov 05 20:56:00 2001 +0100
     2.2 +++ b/src/Provers/induct_method.ML	Mon Nov 05 20:56:29 2001 +0100
     2.3 @@ -106,7 +106,7 @@
     2.4        | (_, _, None) =>
     2.5            let val rules = find_casesS ctxt facts @ find_casesT ctxt insts in
     2.6              if null rules then error "Unable to figure out cases rule" else ();
     2.7 -            Method.trace rules;
     2.8 +            Method.trace ctxt rules;
     2.9              Seq.flat (Seq.map (Seq.try inst_rule) (Seq.of_list rules))
    2.10            end
    2.11        | (_, _, Some r) => Seq.single (inst_rule r));
    2.12 @@ -263,7 +263,7 @@
    2.13          None =>
    2.14            let val rules = find_inductS ctxt facts @ find_inductT ctxt insts in
    2.15              if null rules then error "Unable to figure out induct rule" else ();
    2.16 -            Method.trace rules;
    2.17 +            Method.trace ctxt rules;
    2.18              Seq.flat (Seq.map (Seq.try inst_rule) (Seq.of_list rules))
    2.19            end
    2.20        | Some r => Seq.single (inst_rule r));