tuned;

--- a/src/Pure/Isar/interpretation.ML	Mon Jul 04 19:39:59 2016 +0200
+++ b/src/Pure/Isar/interpretation.ML	Mon Jul 04 19:57:56 2016 +0200
@@ -136,7 +136,7 @@
 
 in
 
-fun generic_interpretation_with_defs prep_interpretation setup_proof note add_registration
+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) =
@@ -145,9 +145,6 @@
       note_eqns_register note add_registration deps witss def_eqns eqns attrss export export';
   in setup_proof after_qed propss eqns goal_ctxt end;
 
-fun generic_interpretation prep_interpretation setup_proof note add_registration expression =
-  generic_interpretation_with_defs prep_interpretation setup_proof note add_registration expression [];
-
 end;
 
 
@@ -168,7 +165,7 @@
   in
     Proof.context_of state
     |> generic_interpretation prep_interpretation setup_proof
-      Attrib.local_notes (Context.proof_map ooo Locale.add_registration) expression raw_eqns
+      Attrib.local_notes (Context.proof_map ooo Locale.add_registration) expression [] raw_eqns
   end;
 
 in
@@ -183,33 +180,33 @@
 
 fun interpretation expression =
   generic_interpretation cert_interpretation Element.witness_proof_eqs
-    Local_Theory.notes_kind Locale.activate_fragment expression;
+    Local_Theory.notes_kind Locale.activate_fragment expression [];
 
-fun interpretation_cmd raw_expression =
+fun interpretation_cmd expression =
   generic_interpretation read_interpretation Element.witness_proof_eqs
-    Local_Theory.notes_kind Locale.activate_fragment raw_expression;
+    Local_Theory.notes_kind Locale.activate_fragment expression [];
 
 
 (* interpretation into global theories *)
 
 fun global_interpretation expression =
-  generic_interpretation_with_defs cert_interpretation Element.witness_proof_eqs
+  generic_interpretation cert_interpretation Element.witness_proof_eqs
     Local_Theory.notes_kind Local_Theory.theory_registration expression;
 
-fun global_interpretation_cmd raw_expression =
-  generic_interpretation_with_defs read_interpretation Element.witness_proof_eqs
-    Local_Theory.notes_kind Local_Theory.theory_registration raw_expression;
+fun global_interpretation_cmd expression =
+  generic_interpretation read_interpretation Element.witness_proof_eqs
+    Local_Theory.notes_kind Local_Theory.theory_registration expression;
 
 
 (* interpretation between locales *)
 
 fun sublocale expression =
-  generic_interpretation_with_defs cert_interpretation Element.witness_proof_eqs
+  generic_interpretation cert_interpretation Element.witness_proof_eqs
     Local_Theory.notes_kind Local_Theory.locale_dependency expression;
 
-fun sublocale_cmd raw_expression =
-  generic_interpretation_with_defs read_interpretation Element.witness_proof_eqs
-    Local_Theory.notes_kind Local_Theory.locale_dependency raw_expression;
+fun sublocale_cmd expression =
+  generic_interpretation read_interpretation Element.witness_proof_eqs
+    Local_Theory.notes_kind Local_Theory.locale_dependency expression;
 
 local
 
@@ -222,7 +219,7 @@
         (fn wits => fn eqs => after_qed wits eqs #> Local_Theory.exit);
   in
     lthy |>
-      generic_interpretation_with_defs prep_interpretation setup_proof
+      generic_interpretation prep_interpretation setup_proof
         Local_Theory.notes_kind Local_Theory.locale_dependency expression raw_defs raw_eqns
   end;
 
@@ -248,7 +245,7 @@
 
 fun gen_isar_interpretation prep_interpretation expression raw_eqns lthy =
   generic_interpretation prep_interpretation Element.witness_proof_eqs
-    Local_Theory.notes_kind (register_or_activate lthy) expression raw_eqns lthy;
+    Local_Theory.notes_kind (register_or_activate lthy) expression [] raw_eqns lthy;
 
 in