# HG changeset patch
# User wenzelm
# Date 1458588127 -3600
# Node ID 45b8dd2d3827a8ec81cba19fb6b8ccdb7ac18a15
# Parent  646b84666a567b66642fd3261ebee058974f7f20
more accurate fixes (e.g. for notE, FalseE), amending baa589c574ff;

diff -r 646b84666a56 -r 45b8dd2d3827 src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Mon Mar 21 19:57:56 2016 +0100
+++ b/src/Pure/Isar/element.ML	Mon Mar 21 20:22:07 2016 +0100
@@ -230,11 +230,13 @@
     val (prems, concl) = Logic.strip_horn prop;
     val concl_term = Object_Logic.drop_judgment ctxt concl;
 
-    val fixes = fold_aterms (fn v as Free (x, T) =>
-        if Variable.is_newly_fixed ctxt' ctxt x andalso not (v aconv concl_term)
-        then insert (op =) (Variable.revert_fixed ctxt' x, T) else I | _ => I) prop [] |> rev;
-    val (assumes, cases) = take_suffix (fn prem =>
-      is_elim andalso concl aconv Logic.strip_assums_concl prem) prems;
+    val (assumes, cases) =
+      take_suffix (fn prem => is_elim andalso concl aconv Logic.strip_assums_concl prem) prems;
+    val is_thesis = if null cases then K false else fn v => v aconv concl_term;
+    val fixes =
+      rev (fold_aterms (fn v as Free (x, T) =>
+        if Variable.is_newly_fixed ctxt' ctxt x andalso not (is_thesis v)
+        then insert (op =) (Variable.revert_fixed ctxt' x, T) else I | _ => I) prop []);
   in
     pretty_ctxt ctxt' (Fixes (map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) fixes)) @
     pretty_ctxt ctxt' (Assumes (map (fn t => (Attrib.empty_binding, [(t, [])])) assumes)) @