1.1 --- a/src/Pure/Isar/method.ML	Tue Sep 07 16:57:52 1999 +0200
     1.2 +++ b/src/Pure/Isar/method.ML	Tue Sep 07 17:21:44 1999 +0200
     1.3 @@ -56,8 +56,7 @@
     1.4      Try of text |
     1.5      Repeat1 of text
     1.6    val refine: text -> Proof.state -> Proof.state Seq.seq
     1.7 -  val tac: text -> Proof.state -> Proof.state Seq.seq
     1.8 -  val then_tac: text -> Proof.state -> Proof.state Seq.seq
     1.9 +  val refine_no_facts: text -> Proof.state -> Proof.state Seq.seq
    1.10    val proof: text option -> Proof.state -> Proof.state Seq.seq
    1.11    val local_qed: text option
    1.12      -> ({kind: string, name: string, thm: thm} -> unit) * (thm -> unit)
    1.13 @@ -321,38 +320,25 @@
    1.14        | eval (Repeat1 txt) = Seq.REPEAT1 (eval txt);
    1.15    in eval text state end;
    1.16  
    1.17 -fun named_method name = Source (Args.src ((name, []), Position.none));
    1.18 +fun refine_no_facts text state =
    1.19 +  state
    1.20 +  |> Proof.goal_facts (K [])
    1.21 +  |> refine text;
    1.22  
    1.23  
    1.24  (* finish *)
    1.25  
    1.26 -local
    1.27 -
    1.28  val FINISHED = FILTER (equal 0 o Thm.nprems_of);
    1.29  val finish = METHOD (K (FINISHED (ALLGOALS assume_tac)));
    1.30  val basic_finish = Basic (K finish);
    1.31  
    1.32 -in
    1.33 -
    1.34  fun finish_text None = basic_finish
    1.35    | finish_text (Some txt) = Then [txt, basic_finish];
    1.36  
    1.37 -end;
    1.38 -
    1.39 -
    1.40 -(* unstructured steps *)
    1.41 -
    1.42 -fun tac text state =
    1.43 -  state
    1.44 -  |> Proof.goal_facts (K [])
    1.45 -  |> refine text;
    1.46 -
    1.47 -val then_tac = refine;
    1.48 -
    1.49  
    1.50  (* structured proof steps *)
    1.51  
    1.52 -val default_text = named_method "default";
    1.53 +val default_text = Source (Args.src (("default", []), Position.none));
    1.54  val assumption_text = Basic (K assumption);
    1.55  
    1.56  fun proof opt_text state =