src/Pure/Isar/proof.ML

     foldl these_facts (st, factss)
     |> put_thms ("prems", prems)
     |> 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
 
 val assm = gen_assume ProofContext.assume;
 val assm_i = gen_assume ProofContext.assume_i;