src/Pure/Isar/method.ML
changeset 9706 8e48a19fc81e
parent 9653 2937a854e3d7
child 9777 232fb8886765
     1.1 --- a/src/Pure/Isar/method.ML	Mon Aug 28 20:31:00 2000 +0200
     1.2 +++ b/src/Pure/Isar/method.ML	Mon Aug 28 20:32:38 2000 +0200
     1.3 @@ -28,7 +28,8 @@
     1.4    val METHOD: (thm list -> tactic) -> Proof.method
     1.5    val METHOD_CASES:
     1.6      (thm list -> thm -> (thm * (string * RuleCases.T) list) Seq.seq) -> Proof.method
     1.7 -  val METHOD0: tactic -> Proof.method
     1.8 +  val SIMPLE_METHOD: tactic -> Proof.method
     1.9 +  val SIMPLE_METHOD': ((int -> tactic) -> tactic) -> (int -> tactic) -> Proof.method
    1.10    val fail: Proof.method
    1.11    val succeed: Proof.method
    1.12    val defer: int option -> Proof.method
    1.13 @@ -80,6 +81,7 @@
    1.14    val thms_ctxt_args: (thm list -> Proof.context -> Proof.method)
    1.15      -> Args.src -> Proof.context -> Proof.method
    1.16    val thms_args: (thm list -> Proof.method) -> Args.src -> Proof.context -> Proof.method
    1.17 +  val thm_args: (thm -> Proof.method) -> Args.src -> Proof.context -> Proof.method
    1.18    datatype text =
    1.19      Basic of (Proof.context -> Proof.method) |
    1.20      Source of Args.src |
    1.21 @@ -212,8 +214,6 @@
    1.22  val METHOD = Proof.method;
    1.23  val METHOD_CASES = Proof.method_cases;
    1.24  
    1.25 -fun METHOD0 tac = METHOD (fn [] => tac | _ => error "Cannot handle current facts");
    1.26 -
    1.27  
    1.28  (* primitive *)
    1.29  
    1.30 @@ -248,13 +248,16 @@
    1.31  end;
    1.32  
    1.33  
    1.34 +(* simple methods *)
    1.35 +
    1.36 +fun SIMPLE_METHOD tac = METHOD (fn facts => ALLGOALS (insert_tac facts) THEN tac);
    1.37 +fun SIMPLE_METHOD' quant tac = METHOD (fn facts => quant (insert_tac facts THEN' tac));
    1.38 +
    1.39 +
    1.40  (* unfold / fold definitions *)
    1.41  
    1.42 -fun unfold thms = METHOD (fn facts =>
    1.43 -  ALLGOALS (insert_tac facts) THEN CHANGED (rewrite_goals_tac thms));
    1.44 -
    1.45 -fun fold thms = METHOD (fn facts =>
    1.46 -  ALLGOALS (insert_tac facts) THEN CHANGED (fold_goals_tac thms));
    1.47 +fun unfold thms = SIMPLE_METHOD (CHANGED (rewrite_goals_tac thms));
    1.48 +fun fold thms = SIMPLE_METHOD (CHANGED (fold_goals_tac thms));
    1.49  
    1.50  
    1.51  (* atomize meta-connectives *)
    1.52 @@ -508,6 +511,7 @@
    1.53  
    1.54  fun thms_ctxt_args f = sectioned_args (thmss []) [] f;
    1.55  fun thms_args f = thms_ctxt_args (K o f);
    1.56 +fun thm_args f = thms_args (fn [thm] => f thm | _ => error "Single theorem expected");
    1.57  
    1.58  end;
    1.59  
    1.60 @@ -523,7 +527,7 @@
    1.61  
    1.62  
    1.63  fun goal_args' args tac = #2 oo syntax (Args.goal_spec HEADGOAL -- args >>
    1.64 -  (fn (quant, s) => METHOD (fn facts => quant (insert_tac facts THEN' tac s))));
    1.65 +  (fn (quant, s) => SIMPLE_METHOD' quant (tac s)));
    1.66  
    1.67  fun goal_args args tac = goal_args' (Scan.lift args) tac;
    1.68  
    1.69 @@ -564,7 +568,7 @@
    1.70  
    1.71  val default_text = Source (Args.src (("default", []), Position.none));
    1.72  val this_text = Basic (K this);
    1.73 -val done_text = Basic (K (METHOD0 all_tac));
    1.74 +val done_text = Basic (K (SIMPLE_METHOD all_tac));
    1.75  
    1.76  fun close_text asm = Basic (fn ctxt => METHOD (K
    1.77    (FILTER Thm.no_prems ((if asm then ALLGOALS (assm_tac ctxt) else all_tac) THEN flexflex_tac))));