src/Pure/Isar/method.ML

 fun tac text state =
   state
   |> Proof.goal_facts (K [])
   |> refine text;
 
-fun then_tac text state =
-  state
-  |> Proof.goal_facts Proof.the_facts
-  |> refine text;
+val then_tac = refine;
 
 
 (* structured proof steps *)
 
 val default_text = named_method "default";