# HG changeset patch
# User wenzelm
# Date 953594276 -3600
# Node ID ac37ba4981527a423ee428e6caece5cac6ad3641
# Parent  b0d2002f9f046c8bd1718c6034246cae2f206bd2
soft_asm_tac: hack to norm goal;

diff -r b0d2002f9f04 -r ac37ba498152 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