# HG changeset patch
# User wenzelm
# Date 1433954928 -7200
# Node ID 014d77e5c1ab0b636768fb07361810ca29c33a88
# Parent  e1ff959f4f1b3fe03874e8319d0b75706cd5ee3b
prefer direct Assumption.add_assms -- avoid term bindings of Proof_Context.add_assms;

diff -r e1ff959f4f1b -r 014d77e5c1ab src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Wed Jun 10 17:22:35 2015 +0200
+++ b/src/Pure/Isar/proof.ML	Wed Jun 10 18:48:48 2015 +0200
@@ -997,23 +997,26 @@
         val (all_propss, binds) = prep_propp fix_ctxt (assumes_propp @ shows_propp);
         val (assumes_propss, shows_propss) = chop (length assumes_propp) all_propss;
 
-        (*prems*)
-        val asms = assumes_bindings ~~ (map o map) (rpair []) assumes_propss;
-        fun note_prems ctxt' =
-          ctxt' |> not (null asms) ?
-            (snd o Proof_Context.note_thmss ""
-              [((Binding.name Auto_Bind.premsN, []), [(Assumption.local_prems_of ctxt' ctxt, [])])]);
-
         (*params*)
-        val (ps, goal_ctxt) = fix_ctxt
+        val (ps, params_ctxt) = fix_ctxt
           |> (fold o fold) Variable.declare_term all_propss
-          |> Proof_Context.add_assms Assumption.assume_export asms |> snd
-          |> note_prems
           |> fold Variable.bind_term binds
           |> fold_map Proof_Context.inferred_param xs';
         val xs = map (Variable.check_name o #1) vars;
         val params = xs ~~ map Free ps;
 
+        (*prems*)
+        val goal_ctxt = params_ctxt
+          |> fold_burrow (Assumption.add_assms Assumption.assume_export)
+              ((map o map) (Thm.cterm_of params_ctxt) assumes_propss)
+          |> (fn (premss, ctxt') => ctxt'
+                |> not (null assumes_propss) ?
+                  (snd o Proof_Context.note_thmss ""
+                    [((Binding.name Auto_Bind.premsN, []),
+                      [(Assumption.local_prems_of ctxt' ctxt, [])])])
+                |> (snd o Proof_Context.note_thmss ""
+                    (assumes_bindings ~~ map (map (fn th => ([th], []))) premss)));
+
         val _ = Variable.warn_extra_tfrees fix_ctxt goal_ctxt;
 
         (*result term bindings*)