aggiornamento for "interpretation with definitions": operate uniformly on theory and locale level under the brand of "permanent interpretation"

--- a/src/HOL/IMP/Abs_Int1_const.thy	Thu Feb 20 12:27:51 2014 +1100
+++ b/src/HOL/IMP/Abs_Int1_const.thy	Wed Feb 19 22:05:05 2014 +0100
@@ -53,7 +53,7 @@
 end
 
 
-interpretation Val_semilattice
+permanent_interpretation Val_semilattice
 where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const
 proof
   case goal1 thus ?case
@@ -67,7 +67,7 @@
     by(auto simp: plus_const_cases split: const.split)
 qed
 
-interpretation Abs_Int
+permanent_interpretation Abs_Int
 where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const
 defines AI_const is AI and step_const is step' and aval'_const is aval'
 ..
@@ -121,7 +121,7 @@
 
 text{* Monotonicity: *}
 
-interpretation Abs_Int_mono
+permanent_interpretation Abs_Int_mono
 where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const
 proof
   case goal1 thus ?case
@@ -133,7 +133,7 @@
 definition m_const :: "const \<Rightarrow> nat" where
 "m_const x = (if x = Any then 0 else 1)"
 
-interpretation Abs_Int_measure
+permanent_interpretation Abs_Int_measure
 where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const
 and m = m_const and h = "1"
 proof

--- a/src/HOL/IMP/Abs_Int1_parity.thy	Thu Feb 20 12:27:51 2014 +1100
+++ b/src/HOL/IMP/Abs_Int1_parity.thy	Wed Feb 19 22:05:05 2014 +0100
@@ -102,7 +102,7 @@
 text{* First we instantiate the abstract value interface and prove that the
 functions on type @{typ parity} have all the necessary properties: *}
 
-interpretation Val_semilattice
+permanent_interpretation Val_semilattice
 where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
 proof txt{* of the locale axioms *}
   fix a b :: parity
@@ -123,7 +123,7 @@
 proofs (they happened in the instatiation above) but delivers the
 instantiated abstract interpreter which we call @{text AI_parity}: *}
 
-interpretation Abs_Int
+permanent_interpretation Abs_Int
 where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
 defines aval_parity is aval' and step_parity is step' and AI_parity is AI
 ..
@@ -154,7 +154,7 @@
 
 subsubsection "Termination"
 
-interpretation Abs_Int_mono
+permanent_interpretation Abs_Int_mono
 where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
 proof
   case goal1 thus ?case
@@ -165,7 +165,7 @@
 definition m_parity :: "parity \<Rightarrow> nat" where
 "m_parity x = (if x = Either then 0 else 1)"
 
-interpretation Abs_Int_measure
+permanent_interpretation Abs_Int_measure
 where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
 and m = m_parity and h = "1"
 proof

--- a/src/HOL/IMP/Abs_Int2_ivl.thy	Thu Feb 20 12:27:51 2014 +1100
+++ b/src/HOL/IMP/Abs_Int2_ivl.thy	Wed Feb 19 22:05:05 2014 +0100
@@ -302,7 +302,7 @@
   "\<lbrakk>Fin y1 \<le> x1; Fin y2 \<le> x2\<rbrakk> \<Longrightarrow> Fin(y1 + y2::'a::ordered_ab_group_add) \<le> x1 + x2"
 by(drule (1) add_mono) simp
 
-interpretation Val_semilattice
+permanent_interpretation Val_semilattice
 where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
 proof
   case goal1 thus ?case by transfer (simp add: le_iff_subset)
@@ -318,7 +318,7 @@
 qed
 
 
-interpretation Val_lattice_gamma
+permanent_interpretation Val_lattice_gamma
 where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
 defines aval_ivl is aval'
 proof
@@ -327,7 +327,7 @@
   case goal2 show ?case unfolding bot_ivl_def by transfer simp
 qed
 
-interpretation Val_inv
+permanent_interpretation Val_inv
 where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
 and test_num' = in_ivl
 and inv_plus' = inv_plus_ivl and inv_less' = inv_less_ivl
@@ -350,7 +350,7 @@
     done
 qed
 
-interpretation Abs_Int_inv
+permanent_interpretation Abs_Int_inv
 where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
 and test_num' = in_ivl
 and inv_plus' = inv_plus_ivl and inv_less' = inv_less_ivl
@@ -384,7 +384,7 @@
 apply(auto simp: below_rep_def le_iff_subset split: if_splits prod.split)
 by(auto simp: is_empty_rep_iff \<gamma>_rep_cases split: extended.splits)
 
-interpretation Abs_Int_inv_mono
+permanent_interpretation Abs_Int_inv_mono
 where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
 and test_num' = in_ivl
 and inv_plus' = inv_plus_ivl and inv_less' = inv_less_ivl

--- a/src/HOL/IMP/Abs_Int3.thy	Thu Feb 20 12:27:51 2014 +1100
+++ b/src/HOL/IMP/Abs_Int3.thy	Wed Feb 19 22:05:05 2014 +0100
@@ -260,7 +260,7 @@
 
 end
 
-interpretation Abs_Int_wn
+permanent_interpretation Abs_Int_wn
 where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
 and test_num' = in_ivl
 and inv_plus' = inv_plus_ivl and inv_less' = inv_less_ivl
@@ -545,7 +545,7 @@
          split: prod.splits if_splits extended.split)
 
 
-interpretation Abs_Int_wn_measure
+permanent_interpretation Abs_Int_wn_measure
 where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
 and test_num' = in_ivl
 and inv_plus' = inv_plus_ivl and inv_less' = inv_less_ivl

--- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_const.thy	Thu Feb 20 12:27:51 2014 +1100
+++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_const.thy	Wed Feb 19 22:05:05 2014 +0100
@@ -47,13 +47,13 @@
 
 end
 
-interpretation Rep rep_cval
+permanent_interpretation Rep rep_cval
 proof
   case goal1 thus ?case
     by(cases a, cases b, simp, simp, cases b, simp, simp)
 qed
 
-interpretation Val_abs rep_cval Const plus_cval
+permanent_interpretation Val_abs rep_cval Const plus_cval
 proof
   case goal1 show ?case by simp
 next
@@ -61,7 +61,7 @@
     by(cases a1, cases a2, simp, simp, cases a2, simp, simp)
 qed
 
-interpretation Abs_Int rep_cval Const plus_cval "(iter' 3)"
+permanent_interpretation Abs_Int rep_cval Const plus_cval "(iter' 3)"
 defines AI_const is AI
 and aval'_const is aval'
 proof qed (auto simp: iter'_pfp_above)

--- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy	Thu Feb 20 12:27:51 2014 +1100
+++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy	Wed Feb 19 22:05:05 2014 +0100
@@ -166,13 +166,13 @@
          I (max_option False (l1 + Some 1) l2) h2)
    else (I (max_option False l1 l2) h1, I l2 (min_option True h1 h2)))"
 
-interpretation Rep rep_ivl
+permanent_interpretation Rep rep_ivl
 proof
   case goal1 thus ?case
     by(auto simp: rep_ivl_def le_ivl_def le_option_def split: ivl.split option.split if_splits)
 qed
 
-interpretation Val_abs rep_ivl num_ivl plus_ivl
+permanent_interpretation Val_abs rep_ivl num_ivl plus_ivl
 proof
   case goal1 thus ?case by(simp add: rep_ivl_def num_ivl_def)
 next
@@ -180,7 +180,7 @@
     by(auto simp add: rep_ivl_def plus_ivl_def split: ivl.split option.splits)
 qed
 
-interpretation Rep1 rep_ivl
+permanent_interpretation Rep1 rep_ivl
 proof
   case goal1 thus ?case
     by(auto simp add: rep_ivl_def meet_ivl_def empty_def min_option_def max_option_def split: ivl.split option.split)
@@ -188,7 +188,7 @@
   case goal2 show ?case by(auto simp add: Bot_ivl_def rep_ivl_def empty_def)
 qed
 
-interpretation
+permanent_interpretation
   Val_abs1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl
 proof
   case goal1 thus ?case
@@ -200,7 +200,7 @@
       auto simp: rep_ivl_def min_option_def max_option_def le_option_def split: if_splits option.splits)
 qed
 
-interpretation
+permanent_interpretation
   Abs_Int1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl "(iter' 3)"
 defines afilter_ivl is afilter
 and bfilter_ivl is bfilter

--- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den2.thy	Thu Feb 20 12:27:51 2014 +1100
+++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den2.thy	Wed Feb 19 22:05:05 2014 +0100
@@ -192,7 +192,7 @@
 
 end
 
-interpretation
+permanent_interpretation
   Abs_Int1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl "(iter' 3 2)"
 defines afilter_ivl' is afilter
 and bfilter_ivl' is bfilter

--- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_const_ITP.thy	Thu Feb 20 12:27:51 2014 +1100
+++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_const_ITP.thy	Wed Feb 19 22:05:05 2014 +0100
@@ -52,7 +52,7 @@
 end
 
 
-interpretation Val_abs
+permanent_interpretation Val_abs
 where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const
 proof
   case goal1 thus ?case
@@ -66,7 +66,7 @@
     by(auto simp: plus_const_cases split: const.split)
 qed
 
-interpretation Abs_Int
+permanent_interpretation Abs_Int
 where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const
 defines AI_const is AI and step_const is step' and aval'_const is aval'
 ..
@@ -114,7 +114,7 @@
 
 text{* Monotonicity: *}
 
-interpretation Abs_Int_mono
+permanent_interpretation Abs_Int_mono
 where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const
 proof
   case goal1 thus ?case

--- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_parity_ITP.thy	Thu Feb 20 12:27:51 2014 +1100
+++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_parity_ITP.thy	Wed Feb 19 22:05:05 2014 +0100
@@ -113,7 +113,7 @@
 proofs (they happened in the instatiation above) but delivers the
 instantiated abstract interpreter which we call AI: *}
 
-interpretation Abs_Int
+permanent_interpretation Abs_Int
 where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
 defines aval_parity is aval' and step_parity is step' and AI_parity is AI
 ..
@@ -141,7 +141,7 @@
 
 subsubsection "Termination"
 
-interpretation Abs_Int_mono
+permanent_interpretation Abs_Int_mono
 where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
 proof
   case goal1 thus ?case

--- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ivl_ITP.thy	Thu Feb 20 12:27:51 2014 +1100
+++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ivl_ITP.thy	Wed Feb 19 22:05:05 2014 +0100
@@ -165,7 +165,7 @@
          I (max_option False (l1 + Some 1) l2) h2)
    else (I (max_option False l1 l2) h1, I l2 (min_option True h1 h2)))"
 
-interpretation Val_abs
+permanent_interpretation Val_abs
 where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
 proof
   case goal1 thus ?case
@@ -179,7 +179,7 @@
     by(auto simp add: \<gamma>_ivl_def plus_ivl_def split: ivl.split option.splits)
 qed
 
-interpretation Val_abs1_gamma
+permanent_interpretation Val_abs1_gamma
 where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
 defines aval_ivl is aval'
 proof
@@ -198,7 +198,7 @@
 done
 
 
-interpretation Val_abs1
+permanent_interpretation Val_abs1
 where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
 and test_num' = in_ivl
 and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl
@@ -215,7 +215,7 @@
       auto simp: \<gamma>_ivl_def min_option_def max_option_def le_option_def split: if_splits option.splits)
 qed
 
-interpretation Abs_Int1
+permanent_interpretation Abs_Int1
 where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
 and test_num' = in_ivl
 and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl
@@ -229,7 +229,7 @@
 
 text{* Monotonicity: *}
 
-interpretation Abs_Int1_mono
+permanent_interpretation Abs_Int1_mono
 where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
 and test_num' = in_ivl
 and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl

--- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int3_ITP.thy	Thu Feb 20 12:27:51 2014 +1100
+++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int3_ITP.thy	Wed Feb 19 22:05:05 2014 +0100
@@ -225,7 +225,7 @@
 
 end
 
-interpretation Abs_Int2
+permanent_interpretation Abs_Int2
 where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
 and test_num' = in_ivl
 and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl

--- a/src/HOL/IMP/Abs_Int_ITP/Collecting_ITP.thy	Thu Feb 20 12:27:51 2014 +1100
+++ b/src/HOL/IMP/Abs_Int_ITP/Collecting_ITP.thy	Wed Feb 19 22:05:05 2014 +0100
@@ -89,7 +89,7 @@
  WHILE b DO lift F c (sub\<^sub>1 ` M)
  {F (post ` M)}"
 
-interpretation Complete_Lattice_ix "%c. {c'. strip c' = c}" "lift Inter"
+permanent_interpretation Complete_Lattice_ix "%c. {c'. strip c' = c}" "lift Inter"
 proof
   case goal1
   have "a:A \<Longrightarrow> lift Inter (strip a) A \<le> a"

--- a/src/HOL/IMP/Collecting.thy	Thu Feb 20 12:27:51 2014 +1100
+++ b/src/HOL/IMP/Collecting.thy	Wed Feb 19 22:05:05 2014 +0100
@@ -95,7 +95,7 @@
 definition Inf_acom :: "com \<Rightarrow> 'a::complete_lattice acom set \<Rightarrow> 'a acom" where
 "Inf_acom c M = annotate (\<lambda>p. INF C:M. anno C p) c"
 
-interpretation
+permanent_interpretation
   Complete_Lattice "{C. strip C = c}" "Inf_acom c" for c
 proof
   case goal1 thus ?case

--- a/src/HOL/ex/Interpretation_with_Defs.thy	Thu Feb 20 12:27:51 2014 +1100
+++ b/src/HOL/ex/Interpretation_with_Defs.thy	Wed Feb 19 22:05:05 2014 +0100
@@ -6,6 +6,7 @@
 
 theory Interpretation_with_Defs
 imports Pure
+keywords "permanent_interpretation" :: thy_goal
 begin
 
 ML_file "~~/src/Tools/interpretation_with_defs.ML"

--- a/src/Tools/interpretation_with_defs.ML	Thu Feb 20 12:27:51 2014 +1100
+++ b/src/Tools/interpretation_with_defs.ML	Wed Feb 19 22:05:05 2014 +0100
@@ -6,87 +6,105 @@
 
 signature INTERPRETATION_WITH_DEFS =
 sig
-  val interpretation: Expression.expression_i ->
+  val permanent_interpretation: Expression.expression_i ->
     (Attrib.binding * ((binding * mixfix) * term)) list -> (Attrib.binding * term) list ->
-    theory -> Proof.state
-  val interpretation_cmd: Expression.expression ->
+    local_theory -> Proof.state
+  val permanent_interpretation_cmd: Expression.expression ->
     (Attrib.binding * ((binding * mixfix) * string)) list -> (Attrib.binding * string) list ->
-    theory -> Proof.state
+    local_theory -> Proof.state
 end;
 
 structure Interpretation_With_Defs : INTERPRETATION_WITH_DEFS =
 struct
 
-fun note_eqns_register deps witss def_eqns attrss eqns export export' =
-  let
-    fun meta_rewrite context =
-      map (Local_Defs.meta_rewrite_rule (Context.proof_of context) #> Drule.abs_def) o
-        maps snd;
-  in
-    Attrib.generic_notes Thm.lemmaK
-      (attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn], [])]) eqns)
-    #-> (fn facts => `(fn context => meta_rewrite context facts))
-    #-> (fn eqns => fold (fn ((dep, morph), wits) =>
-      fn context =>
-        Locale.add_registration
-          (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits))
-          (Element.eq_morphism (Context.theory_of context) (def_eqns @ eqns) |>
-            Option.map (rpair true))
-          export context) (deps ~~ witss))
-  end;
-
 local
 
-fun gen_interpretation prep_expr prep_decl parse_term parse_prop prep_attr
-    expression raw_defs raw_eqns theory =
+(* reading *)
+
+fun prep_interpretation prep_expr prep_term prep_prop prep_attr expression raw_defs raw_eqns initial_ctxt =
   let
-    val (_, (_, defs_ctxt)) =
-      prep_decl expression I [] (Proof_Context.init_global theory);
-
-    val rhss = map (parse_term defs_ctxt o snd o snd) raw_defs
-      |> Syntax.check_terms defs_ctxt;
-    val defs = map2 (fn ((name, atts), ((b, mx), _)) => fn rhs =>
-      ((b, mx), ((Thm.def_binding_optional b name, atts), rhs))) raw_defs rhss;
+    (*reading*)
+    val ((_, deps, _), proto_deps_ctxt) = prep_expr expression initial_ctxt;
+    val deps_ctxt = fold Locale.activate_declarations deps proto_deps_ctxt;
+    val prep = Syntax.check_terms deps_ctxt #> Variable.export_terms deps_ctxt deps_ctxt;
+    val rhss = (prep o map (prep_term deps_ctxt o snd o snd)) raw_defs;
+    val eqns = (prep o map (prep_prop deps_ctxt o snd)) raw_eqns;
 
-    val (def_eqns, theory') = theory
-      |> Named_Target.theory_init
-      |> fold_map (Local_Theory.define) defs
-      |>> map (Thm.symmetric o snd o snd)
-      |> Local_Theory.exit_result_global (map o Morphism.thm);
+    (*defining*)
+    val pre_defs = map2 (fn ((name, atts), ((b, mx), _)) => fn rhs =>
+      ((b, mx), ((Thm.def_binding_optional b name, atts), rhs))) raw_defs rhss;
+    val (defs, defs_ctxt) = fold_map Local_Theory.define pre_defs initial_ctxt;
+    val def_eqns = map (Thm.symmetric o Morphism.thm (Local_Theory.standard_morphism defs_ctxt initial_ctxt) o snd o snd) defs;
+    val base_ctxt = if null def_eqns then defs_ctxt else Local_Theory.restore defs_ctxt;
+      (*the "if" prevents restoring a proof context which is no local theory*)
 
-    val ((propss, deps, export), expr_ctxt) = theory'
-      |> Proof_Context.init_global
-      |> prep_expr expression;
-
-    val eqns = map (parse_prop expr_ctxt o snd) raw_eqns
-      |> Syntax.check_terms expr_ctxt;
-    val attrss = map ((apsnd o map) (prep_attr theory) o fst) raw_eqns;
+    (*setting up*)
+    val ((propss, deps, export), expr_ctxt) = prep_expr expression base_ctxt;
+      (*FIXME: only re-prepare if defs are given*)
+    val attrss = map (apsnd (map (prep_attr (Proof_Context.theory_of expr_ctxt))) o fst) raw_eqns;
     val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
     val export' = Variable.export_morphism goal_ctxt expr_ctxt;
+  in (((propss, deps, export, export'), (def_eqns, eqns, attrss)), goal_ctxt) end;
 
+val cert_interpretation = prep_interpretation Expression.cert_goal_expression (K I) (K I) (K I);
+val read_interpretation = prep_interpretation Expression.read_goal_expression Syntax.parse_term Syntax.parse_prop Attrib.intern_src;
+
+
+(* generic interpretation machinery *)
+
+fun meta_rewrite eqns ctxt = (map (Local_Defs.meta_rewrite_rule ctxt #> Drule.abs_def) (maps snd eqns), ctxt);
+
+fun note_eqns_register note activate deps witss def_eqns eqns attrss export export' ctxt =
+  let
+    val facts = (Attrib.empty_binding, [(map (Morphism.thm (export' $> export)) def_eqns, [])])
+      :: map2 (fn attrs => fn eqn => (attrs, [([Morphism.thm (export' $> export) eqn], [])])) attrss eqns;
+    val (eqns', ctxt') = ctxt
+      |> note Thm.lemmaK facts
+      |-> meta_rewrite;
+    val dep_morphs = map2 (fn (dep, morph) => fn wits =>
+      (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits))) deps witss;
+    fun activate' dep_morph ctxt = activate dep_morph
+      (Option.map (rpair true) (Element.eq_morphism (Proof_Context.theory_of ctxt) eqns')) export ctxt;
+  in
+    ctxt'
+    |> fold activate' dep_morphs
+  end;
+
+fun generic_interpretation prep_interpretation setup_proof note add_registration
+    expression raw_defs raw_eqns initial_ctxt = 
+  let
+    val (((propss, deps, export, export'), (def_eqns, eqns, attrss)), goal_ctxt) = 
+      prep_interpretation expression raw_defs raw_eqns initial_ctxt;
     fun after_qed witss eqns =
-      (Proof_Context.background_theory o Context.theory_map)
-        (note_eqns_register deps witss def_eqns attrss eqns export export');
+      note_eqns_register note add_registration deps witss def_eqns eqns attrss export export';
+  in setup_proof after_qed propss eqns goal_ctxt end;
+
+
+(* interpretation with permanent registration *)
 
-  in Element.witness_proof_eqs after_qed propss eqns goal_ctxt end;
+fun subscribe lthy =
+  if Named_Target.is_theory lthy
+  then Generic_Target.theory_registration
+  else Generic_Target.locale_dependency (Named_Target.the_name lthy);
+
+fun gen_permanent_interpretation prep_interpretation expression raw_defs raw_eqns lthy =
+  generic_interpretation prep_interpretation Element.witness_proof_eqs Local_Theory.notes_kind (subscribe lthy)
+    expression raw_defs raw_eqns lthy
 
 in
 
-fun interpretation x = gen_interpretation Expression.cert_goal_expression
-  Expression.cert_declaration (K I) (K I) (K I) x;
-fun interpretation_cmd x = gen_interpretation Expression.read_goal_expression
-  Expression.read_declaration Syntax.parse_term Syntax.parse_prop Attrib.intern_src x;
+fun permanent_interpretation x = gen_permanent_interpretation cert_interpretation x;
+fun permanent_interpretation_cmd x = gen_permanent_interpretation read_interpretation x;
 
 end;
 
 val _ =
-  Outer_Syntax.command @{command_spec "interpretation"}
-    "prove interpretation of locale expression in theory"
+  Outer_Syntax.local_theory_to_proof @{command_spec "permanent_interpretation"}
+    "prove interpretation of locale expression into named theory"
     (Parse.!!! (Parse_Spec.locale_expression true) --
       Scan.optional (@{keyword "defines"} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":"
         -- ((Parse.binding -- Parse.opt_mixfix') --| @{keyword "is"} -- Parse.term))) [] --
       Scan.optional (Parse.where_ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) []
-      >> (fn ((expr, defs), equations) => Toplevel.print o
-          Toplevel.theory_to_proof (interpretation_cmd expr defs equations)));
+      >> (fn ((expr, defs), eqns) => permanent_interpretation_cmd expr defs eqns));
 
 end;