src/Pure/Isar/local_theory.ML
changeset 59887 43dc3c660f41
parent 59886 e0dc738eb08c
child 59890 01aff5aa081d
--- a/src/Pure/Isar/local_theory.ML	Tue Mar 31 22:31:05 2015 +0200
+++ b/src/Pure/Isar/local_theory.ML	Tue Mar 31 23:42:57 2015 +0200
@@ -222,11 +222,17 @@
 fun raw_theory f = #2 o raw_theory_result (f #> pair ());
 
 fun background_theory_result f lthy =
-  lthy |> raw_theory_result (fn thy =>
-    thy
-    |> Sign.map_naming (K (background_naming_of lthy))
-    |> f
-    ||> Sign.restore_naming thy);
+  let
+    val naming =
+      background_naming_of lthy
+      |> Name_Space.transform_naming (Proof_Context.naming_of lthy);
+  in
+    lthy |> raw_theory_result (fn thy =>
+      thy
+      |> Sign.map_naming (K naming)
+      |> f
+      ||> Sign.restore_naming thy)
+  end;
 
 fun background_theory f = #2 o background_theory_result (f #> pair ());