then_tac = refine;
authorwenzelm
Tue Sep 07 16:57:28 1999 +0200 (1999-09-07)
changeset 75040fec51813079
parent 7503 e8be98558eb8
child 7505 a9690e9cc58a
then_tac = refine;
src/Pure/Isar/method.ML
     1.1 --- a/src/Pure/Isar/method.ML	Tue Sep 07 16:57:15 1999 +0200
     1.2 +++ b/src/Pure/Isar/method.ML	Tue Sep 07 16:57:28 1999 +0200
     1.3 @@ -347,10 +347,7 @@
     1.4    |> Proof.goal_facts (K [])
     1.5    |> refine text;
     1.6  
     1.7 -fun then_tac text state =
     1.8 -  state
     1.9 -  |> Proof.goal_facts Proof.the_facts
    1.10 -  |> refine text;
    1.11 +val then_tac = refine;
    1.12  
    1.13  
    1.14  (* structured proof steps *)