# HG changeset patch
# User haftmann
# Date 1447697318 -3600
# Node ID 91854ba66adb56e05ccfc5e2a37a17987f70c256
# Parent  7ba83fbac0ae3ad58e556c97e7d3cda7affbf72e
clarified contexts by factoring out reading and definition of mixins

diff -r 7ba83fbac0ae -r 91854ba66adb src/Pure/Isar/interpretation.ML
--- a/src/Pure/Isar/interpretation.ML	Mon Nov 16 17:02:12 2015 +0100
+++ b/src/Pure/Isar/interpretation.ML	Mon Nov 16 19:08:38 2015 +0100
@@ -52,25 +52,35 @@
 
 local
 
-fun prep_interpretation prep_expr prep_term prep_prop prep_attr expression raw_defs raw_eqns initial_ctxt =
+fun prep_mixins prep_term prep_prop expr_ctxt deps_ctxt raw_defs raw_eqns =
   let
-    (*reading*)
-    val ((propss, deps, export), expr_ctxt) = prep_expr expression initial_ctxt;
-    val deps_ctxt = fold Locale.activate_declarations deps expr_ctxt;
     val prep = Syntax.check_terms deps_ctxt #> Variable.export_terms deps_ctxt expr_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;
-
-    (*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, forked_ctxt) = fold_map Local_Theory.define pre_defs expr_ctxt;
-    val def_ctxt = Proof_Context.transfer (Proof_Context.theory_of forked_ctxt) expr_ctxt;
-    val def_eqns = defs
-      |> map (Thm.symmetric o
-        Morphism.thm (Local_Theory.standard_morphism forked_ctxt def_ctxt) o snd o snd);
+    val eqns = (prep o map (prep_prop deps_ctxt o snd)) raw_eqns;
+  in (pre_defs, eqns) end;
 
-    (*setting up proof*)
+fun define_mixins [] expr_ctxt = ([], expr_ctxt)
+      (*quasi-inhomogeneous type: definitions demand local theory rather than bare proof context*)
+  | define_mixins pre_defs expr_lthy =
+      let
+        val (defs, forked_lthy) = fold_map Local_Theory.define pre_defs expr_lthy;
+        val def_lthy =
+          Proof_Context.transfer (Proof_Context.theory_of forked_lthy) expr_lthy;
+        val def_eqns = defs
+          |> map (Thm.symmetric o
+              Morphism.thm (Local_Theory.standard_morphism forked_lthy def_lthy) o snd o snd);
+      in (def_eqns, def_lthy) end;
+
+fun prep_interpretation prep_expr prep_term prep_prop prep_attr
+  expression raw_defs raw_eqns initial_ctxt =
+  let
+    val ((propss, deps, export), expr_ctxt) = prep_expr expression initial_ctxt;
+    val (pre_defs, eqns) =
+      prep_mixins prep_term prep_prop expr_ctxt
+        (fold Locale.activate_declarations deps expr_ctxt) raw_defs raw_eqns;
+    val (def_eqns, def_ctxt) = define_mixins pre_defs expr_ctxt;
     val attrss = map (apsnd (map (prep_attr def_ctxt)) o fst) raw_eqns;
     val goal_ctxt = fold Variable.auto_fixes eqns def_ctxt;
     val export' = Variable.export_morphism goal_ctxt def_ctxt;