--- a/src/Pure/Isar/proof.ML Fri Jun 26 18:54:23 2015 +0200
+++ b/src/Pure/Isar/proof.ML Sat Jun 27 00:10:24 2015 +0200
@@ -458,6 +458,14 @@
let fun find i n = if i > n then Seq.fail else Seq.APPEND (tac i, find (i + 1) n)
in find 1 (Thm.nprems_of st) st end;
+fun protect_prem i th =
+ Thm.bicompose NONE {flatten = false, match = false, incremented = true}
+ (false, Drule.incr_indexes th Drule.protectD, 1) i th
+ |> Seq.hd;
+
+fun protect_prems th =
+ fold_rev protect_prem (1 upto Thm.nprems_of th) th;
+
in
fun refine_goals print_rule result_ctxt result state =
@@ -467,6 +475,7 @@
(print_rule goal_ctxt rule; FINDGOAL (goal_tac goal_ctxt rule) st);
in
result
+ |> map (Raw_Simplifier.norm_hhf result_ctxt #> protect_prems)
|> Proof_Context.goal_export result_ctxt goal_ctxt
|> (fn rules => Seq.lift provide_goal (EVERY (map refine rules) goal) state)
end;
@@ -1284,4 +1293,3 @@
end;
end;
-