src/Pure/Isar/isar_syn.ML

         Toplevel.theory_to_proof (Interpretation.sublocale_global_cmd loc expr equations)))
     || interpretation_args >> (fn (expr, equations) =>
         Toplevel.local_theory_to_proof NONE NONE (Interpretation.sublocale_cmd expr equations)));
 
 val _ =
+  Outer_Syntax.local_theory_to_proof @{command_keyword permanent_interpretation}
+    "prove interpretation of locale expression into named theory"
+    (Parse.!!! (Parse_Spec.locale_expression true) --
+      Scan.optional (@{keyword "defining"} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":"
+        -- ((Parse.binding -- Parse.opt_mixfix') --| @{keyword "="} -- Parse.term))) [] --
+      Scan.optional (Parse.where_ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) []
+      >> (fn ((expr, defs), eqns) => Interpretation.permanent_interpretation_cmd expr defs eqns));
+
+val _ =
   Outer_Syntax.command @{command_keyword interpretation}
     "prove interpretation of locale expression in local theory"
     (interpretation_args >> (fn (expr, equations) =>
       Toplevel.local_theory_to_proof NONE NONE (Interpretation.interpretation_cmd expr equations)));