# HG changeset patch
# User wenzelm
# Date 1333464661 -7200
# Node ID 008b7858f3c0d00f93af63597fa2360c5220bd78
# Parent  052cd5f1a591d0e546833889b9f9af59546ddf73
retain literal non-HHF assumptions, to facilitate re-import in Generic_Target.import_export_proof;

diff -r 052cd5f1a591 -r 008b7858f3c0 src/Pure/Isar/local_defs.ML
--- a/src/Pure/Isar/local_defs.ML	Tue Apr 03 16:49:05 2012 +0200
+++ b/src/Pure/Isar/local_defs.ML	Tue Apr 03 16:51:01 2012 +0200
@@ -135,22 +135,22 @@
   let
     val exp = Assumption.export false inner outer;
     val exp_term = Assumption.export_term inner outer;
-    val prems = Assumption.local_prems_of inner outer;
+    val asms = Assumption.local_assms_of inner outer;
   in
     fn th =>
       let
         val th' = exp th;
-        val defs_asms = prems |> map (fn prem =>
-          (case try (head_of_def o Thm.prop_of) prem of
-            NONE => (prem, false)
+        val defs_asms = asms |> map (Thm.assume #> (fn asm =>
+          (case try (head_of_def o Thm.prop_of) asm of
+            NONE => (asm, false)
           | SOME x =>
               let val t = Free x in
                 (case try exp_term t of
-                  NONE => (prem, false)
+                  NONE => (asm, false)
                 | SOME u =>
-                    if t aconv u then (prem, false)
-                    else (Drule.abs_def prem, true))
-              end));
+                    if t aconv u then (asm, false)
+                    else (Drule.abs_def asm, true))
+              end)));
       in (pairself (map #1) (List.partition #2 defs_asms), th') end
   end;