# HG changeset patch
# User wenzelm
# Date 1152221800 -7200
# Node ID 2087e56345983ca7691945bc31470566a2317295
# Parent  f5c39548101e004384c45ad507523ab45ba46c31
removed obsolete locale view;

diff -r f5c39548101e -r 2087e5634598 src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Thu Jul 06 17:47:35 2006 +0200
+++ b/src/Pure/Isar/local_theory.ML	Thu Jul 06 23:36:40 2006 +0200
@@ -56,7 +56,7 @@
 (
   val name = "Pure/local_theory";
   type T =
-   {locale: (string * (cterm list * Proof.context)) option,
+   {locale: (string * Proof.context) option,
     params: (string * typ) list,
     hyps: term list,
     restore_naming: theory -> theory};
@@ -66,7 +66,7 @@
 val _ = Context.add_setup Data.init;
 
 fun map_locale f = Data.map (fn {locale, params, hyps, restore_naming} =>
-  {locale = Option.map (fn (loc, (view, ctxt)) => (loc, (view, f ctxt))) locale,
+  {locale = Option.map (fn (loc, ctxt) => (loc, f ctxt)) locale,
     params = params, hyps = hyps, restore_naming = restore_naming});
 
 val locale_of = #locale o Data.get;
@@ -76,7 +76,7 @@
 fun standard ctxt =
   (case #locale (Data.get ctxt) of
     NONE => map Drule.standard
-  | SOME (_, (_, loc_ctxt)) => ProofContext.export_standard ctxt loc_ctxt);
+  | SOME (_, loc_ctxt) => ProofContext.export_standard ctxt loc_ctxt);
 
 
 (* print consts *)
@@ -116,9 +116,9 @@
 fun locale_result f ctxt =
   (case locale_of ctxt of
     NONE => error "Local theory: no locale context"
-  | SOME (_, view_ctxt) =>
+  | SOME (_, loc_ctxt) =>
       let
-        val (res, loc_ctxt') = f view_ctxt;
+        val (res, loc_ctxt') = f loc_ctxt;
         val thy' = ProofContext.theory_of loc_ctxt';
       in (res, ctxt |> map_locale (K loc_ctxt') |> ProofContext.transfer thy') end);
 
@@ -132,10 +132,10 @@
 fun init_i NONE thy = ProofContext.init thy
   | init_i (SOME loc) thy =
       thy
-      |> (fn thy => ([], Locale.init loc thy))
-      ||>> ProofContext.inferred_fixes
-      |> (fn ((view, params), ctxt) => Data.put
-          {locale = SOME (loc, (view, ctxt)),
+      |> Locale.init loc
+      |> ProofContext.inferred_fixes
+      |> (fn (params, ctxt) => Data.put
+          {locale = SOME (loc, ctxt),
            params = params,
            hyps = ProofContext.assms_of ctxt,
            restore_naming = Sign.restore_naming thy} ctxt);
@@ -145,7 +145,7 @@
 fun restore ctxt =
   (case locale_of ctxt of
     NONE => ctxt
-  | SOME (_, (_, loc_ctxt)) => loc_ctxt |> Data.put (Data.get ctxt));
+  | SOME (_, loc_ctxt) => loc_ctxt |> Data.put (Data.get ctxt));
 
 fun exit ctxt = (ctxt, ProofContext.theory_of ctxt);
 
@@ -216,7 +216,7 @@
     (case locale_of ctxt of
       NONE => theory_result (PureThy.note_thmss_i kind (Attrib.map_facts attrib facts'))
     | SOME (loc, _) =>
-        locale_result (apfst #1 o (fn (_, ctxt) => Locale.add_thmss kind loc facts' ctxt)))
+        locale_result (apfst #1 o Locale.add_thmss kind loc facts'))
     ||> (#2 o ProofContext.note_thmss_i (Attrib.map_facts attrib facts))
   end;
 
diff -r f5c39548101e -r 2087e5634598 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Thu Jul 06 17:47:35 2006 +0200
+++ b/src/Pure/Isar/locale.ML	Thu Jul 06 23:36:40 2006 +0200
@@ -95,8 +95,7 @@
     ((string * Attrib.src list) * (thm list * Attrib.src list) list) list ->
     Proof.context ->
     ((string * thm list) list * (string * thm list) list) * Proof.context
-  val add_term_syntax: string -> (Proof.context -> Proof.context) ->
-    cterm list * Proof.context -> Proof.context
+  val add_term_syntax: string -> (Proof.context -> Proof.context) -> Proof.context -> Proof.context
 
   val theorem: string -> Method.text option -> (thm list list -> theory -> theory) ->
     string * Attrib.src list -> Element.context element list -> Element.statement ->
@@ -1562,7 +1561,7 @@
 (* term syntax *)
 
 fun add_term_syntax loc syn =
-  snd #> syn #> ProofContext.map_theory (change_locale loc
+  syn #> ProofContext.map_theory (change_locale loc
     (fn (axiom, import, elems, params, lparams, term_syntax, regs, intros) =>
       (axiom, import, elems, params, lparams, (syn, stamp ()) :: term_syntax, regs, intros)));
 
@@ -1581,7 +1580,7 @@
 fun theory_results kind prefix results ctxt thy =
   let
     val thy_ctxt = ProofContext.init thy;
-    val export = ProofContext.export_view [] ctxt thy_ctxt;
+    val export = singleton (ProofContext.export_standard ctxt thy_ctxt);
     val facts = map (fn (name, ths) => ((name, []), [(map export ths, [])])) results;
   in thy |> PureThy.note_thmss_qualified kind prefix facts end;
 
@@ -1904,9 +1903,7 @@
     val thy_ctxt = ProofContext.init thy;
     val elems = map (prep_elem thy) (raw_elems @ concl_elems);
     val (_, _, ctxt, propp) = prep_stmt NONE elems (map snd concl) thy_ctxt;
-    val ((stmt, facts), goal_ctxt) = ctxt
-      |> ProofContext.add_view thy_ctxt []
-      |> mk_stmt (map fst concl ~~ propp);
+    val ((stmt, facts), goal_ctxt) = mk_stmt (map fst concl ~~ propp) ctxt;
   in
     global_goal kind before_qed after_qed (SOME "") (name, atts) stmt goal_ctxt
     |> Proof.refine_insert facts
@@ -1926,18 +1923,13 @@
     val thy_ctxt = init_term_syntax loc (ProofContext.init thy);
     val (_, loc_ctxt, elems_ctxt, propp) =
       prep_stmt (SOME raw_loc) elems (map snd concl) thy_ctxt;
-    val elems_ctxt' = elems_ctxt
-      |> ProofContext.add_view loc_ctxt []
-      |> ProofContext.add_view thy_ctxt [];
-    val loc_ctxt' = loc_ctxt
-      |> ProofContext.add_view thy_ctxt [];
 
     val ((stmt, facts), goal_ctxt) =
-      elems_ctxt' |> mk_stmt (map (apsnd (K []) o fst) concl ~~ propp);
+      mk_stmt (map (apsnd (K []) o fst) concl ~~ propp) elems_ctxt;
 
     fun after_qed' results =
       let val loc_results = results |> map
-          (ProofContext.export_standard goal_ctxt loc_ctxt') in
+          (ProofContext.export_standard goal_ctxt loc_ctxt) in
         curry (locale_results kind loc ((names ~~ loc_attss) ~~ loc_results)) loc_ctxt
         #-> (fn res =>
           if name = "" andalso null loc_atts then I