1.1 --- a/src/Pure/Isar/proof.ML	Mon Mar 20 18:49:14 2000 +0100
     1.2 +++ b/src/Pure/Isar/proof.ML	Tue Mar 21 00:17:56 2000 +0100
     1.3 @@ -545,7 +545,8 @@
     1.4      |> put_facts (Some (flat (map #2 factss))));
     1.5  
     1.6  val hard_asm_tac = Tactic.etac Drule.triv_goal;
     1.7 -val soft_asm_tac = Tactic.rtac Drule.triv_goal;
     1.8 +val soft_asm_tac = Tactic.rtac Drule.triv_goal
     1.9 +  THEN' Tactic.rtac asm_rl;	(* FIXME hack to norm goal *)
    1.10  
    1.11  in
    1.12