src/Pure/Isar/proof.ML

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