src/Pure/Isar/locale.ML

     theory -> ((string * thm list) list * (string * thm list) list) * (Proof.context * theory)
   val add_thmss: string -> string ->
     ((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 ->
     theory -> Proof.state
   val theorem_i: string -> Method.text option -> (thm list list -> theory -> theory) ->

 
 
 (* 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)));
 
 fun init_term_syntax loc ctxt =
   fold_rev (fn (f, _) => fn ctxt' => f ctxt')

 (* theory/locale results *)
 
 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;
 
 local
 

     val atts = map (prep_src thy) raw_atts;
     val ((concl_elems, concl), mk_stmt) = conclusion (prep_src thy) raw_concl;
     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
   end;
 

     val names = map (fst o fst) concl;
 
     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
           else #2 o locale_results kind loc [((name, loc_atts), maps #2 res)])
         #> #2