src/Pure/Isar/method.ML
changeset 21687 f689f729afab
parent 21592 8831206d7f41
child 21879 a3efbae45735
     1.1 --- a/src/Pure/Isar/method.ML	Wed Dec 06 21:19:03 2006 +0100
     1.2 +++ b/src/Pure/Isar/method.ML	Thu Dec 07 00:42:04 2006 +0100
     1.3 @@ -140,9 +140,9 @@
     1.4  fun RAW_METHOD tac = RAW_METHOD_CASES (NO_CASES o tac);
     1.5  
     1.6  fun METHOD_CASES tac = RAW_METHOD_CASES (fn facts =>
     1.7 -  Seq.THEN (ALLGOALS Tactic.conjunction_tac, tac facts));
     1.8 +  Seq.THEN (ALLGOALS Goal.conjunction_tac, tac facts));
     1.9  
    1.10 -fun METHOD tac = RAW_METHOD (fn facts => ALLGOALS Tactic.conjunction_tac THEN tac facts);
    1.11 +fun METHOD tac = RAW_METHOD (fn facts => ALLGOALS Goal.conjunction_tac THEN tac facts);
    1.12  
    1.13  val fail = METHOD (K no_tac);
    1.14  val succeed = METHOD (K all_tac);
    1.15 @@ -256,7 +256,7 @@
    1.16    (fn i => fn st =>
    1.17      if null facts then tac rules i st
    1.18      else Seq.maps (fn rule => (tac o single) rule i st) (Drule.multi_resolves facts rules))
    1.19 -  THEN_ALL_NEW Tactic.norm_hhf_tac;
    1.20 +  THEN_ALL_NEW Goal.norm_hhf_tac;
    1.21  
    1.22  fun gen_arule_tac tac j rules facts =
    1.23    EVERY' (gen_rule_tac tac rules facts :: replicate j Tactic.assume_tac);