Method.refine_no_facts;

--- a/src/Pure/Isar/isar_thy.ML	Tue Sep 07 16:57:52 1999 +0200
+++ b/src/Pure/Isar/isar_thy.ML	Tue Sep 07 17:21:44 1999 +0200
@@ -326,8 +326,8 @@
 
 (* backward steps *)
 
-val tac = ProofHistory.applys o Method.tac;
-val then_tac = ProofHistory.applys o Method.then_tac;
+val tac = ProofHistory.applys o Method.refine_no_facts;
+val then_tac = ProofHistory.applys o Method.refine;
 
 val proof = ProofHistory.applys o Method.proof o
   apsome Comment.ignore_interest o Comment.ignore_interest' o Comment.ignore;

--- a/src/Pure/Isar/method.ML	Tue Sep 07 16:57:52 1999 +0200
+++ b/src/Pure/Isar/method.ML	Tue Sep 07 17:21:44 1999 +0200
@@ -56,8 +56,7 @@
     Try of text |
     Repeat1 of text
   val refine: text -> Proof.state -> Proof.state Seq.seq
-  val tac: text -> Proof.state -> Proof.state Seq.seq
-  val then_tac: text -> Proof.state -> Proof.state Seq.seq
+  val refine_no_facts: text -> Proof.state -> Proof.state Seq.seq
   val proof: text option -> Proof.state -> Proof.state Seq.seq
   val local_qed: text option
     -> ({kind: string, name: string, thm: thm} -> unit) * (thm -> unit)
@@ -321,38 +320,25 @@
       | eval (Repeat1 txt) = Seq.REPEAT1 (eval txt);
   in eval text state end;
 
-fun named_method name = Source (Args.src ((name, []), Position.none));
+fun refine_no_facts text state =
+  state
+  |> Proof.goal_facts (K [])
+  |> refine text;
 
 
 (* finish *)
 
-local
-
 val FINISHED = FILTER (equal 0 o Thm.nprems_of);
 val finish = METHOD (K (FINISHED (ALLGOALS assume_tac)));
 val basic_finish = Basic (K finish);
 
-in
-
 fun finish_text None = basic_finish
   | finish_text (Some txt) = Then [txt, basic_finish];
 
-end;
-
-
-(* unstructured steps *)
-
-fun tac text state =
-  state
-  |> Proof.goal_facts (K [])
-  |> refine text;
-
-val then_tac = refine;
-
 
 (* structured proof steps *)
 
-val default_text = named_method "default";
+val default_text = Source (Args.src (("default", []), Position.none));
 val assumption_text = Basic (K assumption);
 
 fun proof opt_text state =