src/Pure/Isar/locale.ML

--- a/src/Pure/Isar/locale.ML	Tue May 16 21:33:14 2006 +0200
+++ b/src/Pure/Isar/locale.ML	Tue May 16 21:33:16 2006 +0200
@@ -87,7 +87,7 @@
     ((string * Attrib.src list) * (thm list * Attrib.src list) list) list ->
     cterm list * Proof.context ->
     ((string * thm list) list * (string * thm list) list) * Proof.context
-  val add_abbrevs: string -> string * bool -> (bstring * term * mixfix) list ->
+  val add_term_syntax: string -> (Proof.context -> Proof.context) ->
     cterm list * Proof.context -> Proof.context
 
   val theorem: string -> Method.text option -> (thm list list -> theory -> theory) ->
@@ -150,7 +150,7 @@
   elems: (Element.context_i * stamp) list,                          (*static content*)
   params: ((string * typ) * mixfix) list,                           (*all params*)
   lparams: string list,                                             (*local parmas*)
-  abbrevs: (((string * bool) * (bstring * term * mixfix) list) * stamp) list,  (*abbreviations*)
+  term_syntax: ((Proof.context -> Proof.context) * stamp) list, (* FIXME depend on morphism *)
   regs: ((string * string list) * (term * thm) list) list}
     (* Registrations: indentifiers and witness theorems of locales interpreted
        in the locale.
@@ -267,14 +267,14 @@
   val copy = I;
   val extend = I;
 
-  fun join_locs _ ({predicate, import, elems, params, lparams, abbrevs, regs}: locale,
-      {elems = elems', abbrevs = abbrevs', regs = regs', ...}: locale) =
+  fun join_locs _ ({predicate, import, elems, params, lparams, term_syntax, regs}: locale,
+      {elems = elems', term_syntax = term_syntax', regs = regs', ...}: locale) =
      {predicate = predicate,
       import = import,
       elems = gen_merge_lists (eq_snd (op =)) elems elems',
       params = params,
       lparams = lparams,
-      abbrevs = Library.merge (eq_snd (op =)) (abbrevs, abbrevs'),
+      term_syntax = Library.merge (eq_snd (op =)) (term_syntax, term_syntax'),
       regs = merge_alists regs regs'};
   fun merge _ ((space1, locs1, regs1), (space2, locs2, regs2)) =
     (NameSpace.merge (space1, space2), Symtab.join join_locs (locs1, locs2),
@@ -327,12 +327,12 @@
 
 fun change_locale name f thy =
   let
-    val {predicate, import, elems, params, lparams, abbrevs, regs} = the_locale thy name;
-    val (predicate', import', elems', params', lparams', abbrevs', regs') =
-      f (predicate, import, elems, params, lparams, abbrevs, regs);
+    val {predicate, import, elems, params, lparams, term_syntax, regs} = the_locale thy name;
+    val (predicate', import', elems', params', lparams', term_syntax', regs') =
+      f (predicate, import, elems, params, lparams, term_syntax, regs);
   in
     put_locale name {predicate = predicate', import = import', elems = elems',
-      params = params', lparams = lparams', abbrevs = abbrevs', regs = regs'} thy
+      params = params', lparams = lparams', term_syntax = term_syntax', regs = regs'} thy
   end;
 
 
@@ -397,8 +397,8 @@
      gen_put_registration LocalLocalesData.map ProofContext.theory_of;
 
 fun put_registration_in_locale name id =
-  change_locale name (fn (predicate, import, elems, params, lparams, abbrevs, regs) =>
-    (predicate, import, elems, params, lparams, abbrevs, regs @ [(id, [])]));
+  change_locale name (fn (predicate, import, elems, params, lparams, term_syntax, regs) =>
+    (predicate, import, elems, params, lparams, term_syntax, regs @ [(id, [])]));
 
 
 (* add witness theorem to registration in theory or context,
@@ -413,11 +413,11 @@
 val add_local_witness = LocalLocalesData.map oo add_witness;
 
 fun add_witness_in_locale name id thm =
-  change_locale name (fn (predicate, import, elems, params, lparams, abbrevs, regs) =>
+  change_locale name (fn (predicate, import, elems, params, lparams, term_syntax, regs) =>
     let
       fun add (id', thms) =
         if id = id' then (id', thm :: thms) else (id', thms);
-    in (predicate, import, elems, params, lparams, abbrevs, map add regs) end);
+    in (predicate, import, elems, params, lparams, term_syntax, map add regs) end);
 
 
 (* printing of registrations *)
@@ -1487,21 +1487,20 @@
   in fold activate regs thy end;
 
 
-(* abbreviations *)
+(* term syntax *)
 
-fun add_abbrevs loc prmode decls =
-  snd #> ProofContext.add_abbrevs_i prmode decls #>
-  ProofContext.map_theory (change_locale loc
-    (fn (predicate, import, elems, params, lparams, abbrevs, regs) =>
-      (predicate, import, elems, params, lparams, ((prmode, decls), stamp ()) :: abbrevs, regs)));
+fun add_term_syntax loc syn =
+  snd #> syn #> ProofContext.map_theory (change_locale loc
+    (fn (predicate, import, elems, params, lparams, term_syntax, regs) =>
+      (predicate, import, elems, params, lparams, (syn, stamp ()) :: term_syntax, regs)));
 
-fun init_abbrevs loc ctxt =
-  fold_rev (uncurry ProofContext.add_abbrevs_i o fst)
-    (#abbrevs (the_locale (ProofContext.theory_of ctxt) loc)) ctxt;
+fun init_term_syntax loc ctxt =
+  fold_rev (fn (f, _) => fn ctxt' => f ctxt')
+    (#term_syntax (the_locale (ProofContext.theory_of ctxt) loc)) ctxt;
 
 fun init loc =
   ProofContext.init
-  #> init_abbrevs loc
+  #> init_term_syntax loc
   #> (#2 o cert_context_statement (SOME loc) [] []);
 
 
@@ -1522,8 +1521,8 @@
       activate_facts prep_facts (ctxt, [((("", []), Assumed []), [Ext (Notes args)])]);
     val (facts', thy') =
       thy
-      |> change_locale loc (fn (predicate, import, elems, params, lparams, abbrevs, regs) =>
-        (predicate, import, elems @ [(Notes args', stamp ())], params, lparams, abbrevs, regs))
+      |> change_locale loc (fn (predicate, import, elems, params, lparams, term_syntax, regs) =>
+        (predicate, import, elems @ [(Notes args', stamp ())], params, lparams, term_syntax, regs))
       |> note_thmss_registrations kind loc args'
       |> global_results (map (#1 o #1) args' ~~ map #2 facts) (view, ctxt);
   in ((facts, facts'), (ProofContext.transfer thy' ctxt', thy')) end;
@@ -1744,7 +1743,7 @@
         elems = map (fn e => (e, stamp ())) elems',
         params = params_of elemss' |> map (fn (x, SOME T) => ((x, T), the (Symtab.lookup syn x))),
         lparams = map #1 (params_of body_elemss),
-        abbrevs = [],
+        term_syntax = [],
         regs = []};
   in ((name, ProofContext.transfer thy' body_ctxt), thy') end;
 
@@ -1802,7 +1801,7 @@
     val elems = map (prep_elem thy) (raw_elems @ concl_elems);
     val names = map (fst o fst) concl;
 
-    val thy_ctxt = init_abbrevs loc (ProofContext.init thy);
+    val thy_ctxt = init_term_syntax loc (ProofContext.init thy);
     val (_, (loc_view, loc_ctxt), (elems_view, elems_ctxt), propp) =
       prep_stmt (SOME raw_loc) elems (map snd concl) thy_ctxt;
     val elems_ctxt' = elems_ctxt