src/Pure/Isar/locale.ML

        from the locale predicate to the normalised assumptions of the locale
        (cf. [1], normalisation of locale expressions.)
     *)
   import: expr,                                                     (*dynamic import*)
   elems: (Element.context_i * stamp) list,                          (*static content*)
-  params: ((string * typ) * mixfix) list * string list,             (*all/local params*)
+  params: ((string * typ) * mixfix) list,                           (*all params*)
+  lparams: string list,                                             (*local parmas*)
   abbrevs: ((bool * (bstring * term * mixfix) list) * stamp) list,  (*abbreviations*)
   regs: ((string * string list) * (term * thm) list) list}
     (* Registrations: indentifiers and witness theorems of locales interpreted
        in the locale.
     *)

 
   val empty = (NameSpace.empty, Symtab.empty, Symtab.empty);
   val copy = I;
   val extend = I;
 
-  fun join_locs _ ({predicate, import, elems, params, abbrevs, regs}: locale,
+  fun join_locs _ ({predicate, import, elems, params, lparams, abbrevs, regs}: locale,
       {elems = elems', abbrevs = abbrevs', 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'),
       regs = merge_alists regs regs'};
   fun merge _ ((space1, locs1, regs1), (space2, locs2, regs2)) =
     (NameSpace.merge (space1, space2), Symtab.join join_locs (locs1, locs2),
      Symtab.join (K Registrations.join) (regs1, regs2));

     SOME loc => loc
   | NONE => error ("Unknown locale " ^ quote name));
 
 fun change_locale name f thy =
   let
-    val {predicate, import, elems , params, abbrevs, regs} = the_locale thy name;
-    val (predicate', import', elems', params', abbrevs', regs') =
-      f (predicate, import, elems, params, abbrevs, regs);
+    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);
   in
     put_locale name {predicate = predicate', import = import', elems = elems',
-      params = params', abbrevs = abbrevs', regs = regs'} thy
+      params = params', lparams = lparams', abbrevs = abbrevs', regs = regs'} thy
   end;
 
 
 (* access registrations *)
 

        GlobalLocalesData.map (fn (space, locs, regs) => (space, locs, f regs))) I;
 val put_local_registration =
      gen_put_registration LocalLocalesData.map ProofContext.theory_of;
 
 fun put_registration_in_locale name id =
-  change_locale name (fn (predicate, import, elems, params, abbrevs, regs) =>
-    (predicate, import, elems, params, abbrevs, regs @ [(id, [])]));
+  change_locale name (fn (predicate, import, elems, params, lparams, abbrevs, regs) =>
+    (predicate, import, elems, params, lparams, abbrevs, regs @ [(id, [])]));
 
 
 (* add witness theorem to registration in theory or context,
    ignored if registration not present *)
 

   GlobalLocalesData.map (fn (space, locs, regs) => (space, locs, add_witness id thm regs));
 
 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, abbrevs, regs) =>
+  change_locale name (fn (predicate, import, elems, params, lparams, abbrevs, regs) =>
     let
       fun add (id', thms) =
         if id = id' then (id', thm :: thms) else (id', thms);
-    in (predicate, import, elems, params, abbrevs, map add regs) end);
+    in (predicate, import, elems, params, lparams, abbrevs, map add regs) end);
 
 
 (* printing of registrations *)
 
 fun gen_print_registrations get_regs mk_ctxt msg show_wits loc thy_ctxt =

        adjust hyps of witness theorems *)
 
     fun add_regs (name, ps) (ths, ids) =
         let
           val {params, regs, ...} = the_locale thy name;
-          val ps' = map #1 (#1 params);
+          val ps' = map #1 params;
           val ren = map #1 ps' ~~ map (fn (x, _) => (x, NONE)) ps;
             (* dummy syntax, since required by rename *)
           val ps'' = map (fn ((p, _), (_, T)) => (p, T)) (ps ~~ ps');
           val [env] = unify_parms ctxt ps [map (apsnd SOME) ps''];
             (* propagate parameter types, to keep them consistent *)

        identify at top level (top = true);
        parms is accumulated list of parameters *)
           let
             val {predicate = (_, axioms), import, params, ...} =
               the_locale thy name;
-            val ps = map (#1 o #1) (#1 params);
+            val ps = map (#1 o #1) params;
             val (ids', parms', _) = identify false import;
                 (* acyclic import dependencies *)
             val ids'' = ids' @ [((name, ps), ([], Assumed []))];
-            val (_, ids''') = add_regs (name, map #1 (#1 params)) ([], ids'');
+            val (_, ids''') = add_regs (name, map #1 params) ([], ids'');
 
             val ids_ax = if top then fst
                  (fold_map (axiomify ps) ids''' axioms)
               else ids''';
-            val syn = Symtab.make (map (apfst fst) (#1 params));
+            val syn = Symtab.make (map (apfst fst) params);
             in (ids_ax, merge_lists parms' ps, syn) end
       | identify top (Rename (e, xs)) =
           let
             val (ids', parms', syn') = identify top e;
             val ren = renaming xs parms'

        the corresponding elements (with renamed parameters),
        also takes care of parameter syntax *)
 
     fun eval syn ((name, xs), axs) =
       let
-        val {params = (ps, qs), elems, ...} = the_locale thy name;
+        val {params = ps, lparams = qs, elems, ...} = the_locale thy name;
         val ps' = map (apsnd SOME o #1) ps;
         fun lookup_syn x = (case Symtab.lookup syn x of SOME Structure => NONE | opt => opt);
         val ren = map #1 ps' ~~ map (fn x => (x, lookup_syn x)) xs;
         val (params', elems') =
           if null ren then ((ps', qs), map #1 elems)

   end;
 
 in
 
 fun parameters_of thy name =
-  the_locale thy name |> #params |> fst;
+  the_locale thy name |> #params;
 
 fun parameters_of_expr thy expr =
   let
     val ctxt = ProofContext.init thy;
     val ((_, syn), raw_elemss) = flatten (ctxt, intern_expr thy)

     val locale = Option.map (prep_locale thy) raw_locale;
     val (locale_stmt, fixed_params, import) =
       (case locale of
         NONE => ([], [], empty)
       | SOME name =>
-          let val {predicate = (stmt, _), params = (ps, _), ...} = the_locale thy name
+          let val {predicate = (stmt, _), params = ps, ...} = the_locale thy name
           in (stmt, map fst ps, Locale name) end);
     val ((((locale_ctxt, _), (elems_ctxt, _, _)), _), (elems_stmt, concl')) =
       prep_ctxt false fixed_params import elems concl ctxt;
   in (locale, (locale_stmt, locale_ctxt), (elems_stmt, elems_ctxt), concl') end;
 

 (* store instantiations of args for all registered interpretations
    of the theory *)
 
 fun note_thmss_registrations kind target args thy =
   let
-    val parms = the_locale thy target |> #params |> fst |> map fst;
+    val parms = the_locale thy target |> #params |> map fst;
     val ids = flatten (ProofContext.init thy, intern_expr thy)
       (([], Symtab.empty), Expr (Locale target)) |> fst |> fst
       |> List.mapPartial (fn (id, (_, Assumed _)) => SOME id | _ => NONE)
 
     val regs = get_global_registrations thy target;

 (* abbreviations *)
 
 fun add_abbrevs loc revert decls =
   snd #> ProofContext.add_abbrevs_i revert decls #>
   ProofContext.map_theory (change_locale loc
-    (fn (predicate, import, elems, params, abbrevs, regs) =>
-      (predicate, import, elems, params, ((revert, decls), stamp ()) :: abbrevs, regs)));
+    (fn (predicate, import, elems, params, lparams, abbrevs, regs) =>
+      (predicate, import, elems, params, lparams, ((revert, decls), stamp ()) :: abbrevs, regs)));
 
 fun init_abbrevs loc ctxt =
   fold_rev (uncurry ProofContext.add_abbrevs_i o fst)
     (#abbrevs (the_locale (ProofContext.theory_of ctxt) loc)) ctxt;
 

   let
     val (ctxt', ([(_, [Notes args'])], facts)) =
       activate_facts prep_facts (ctxt, [((("", []), Assumed []), [Ext (Notes args)])]);
     val (facts', thy') =
       thy
-      |> change_locale loc (fn (predicate, import, elems, params, abbrevs, regs) =>
-        (predicate, import, elems @ [(Notes args', stamp ())], params, abbrevs, regs))
+      |> change_locale loc (fn (predicate, import, elems, params, lparams, abbrevs, regs) =>
+        (predicate, import, elems @ [(Notes args', stamp ())], params, lparams, abbrevs, 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;
 
 fun gen_note prep_locale prep_facts kind raw_loc args thy =

       |> declare_locale name
       |> put_locale name
        {predicate = predicate,
         import = import,
         elems = map (fn e => (e, stamp ())) elems',
-        params = (params_of elemss' |> map (fn (x, SOME T) => ((x, T), the (Symtab.lookup syn x))),
-          map #1 (params_of body_elemss)),
+        params = params_of elemss' |> map (fn (x, SOME T) => ((x, T), the (Symtab.lookup syn x))),
+        lparams = map #1 (params_of body_elemss),
         abbrevs = [],
         regs = []};
   in (ProofContext.transfer thy' body_ctxt, thy') end;
 
 in

   (* target already in internal form *)
   let
     val ctxt = ProofContext.init thy;
     val ((raw_target_ids, target_syn), _) = flatten (ctxt, I)
         (([], Symtab.empty), Expr (Locale target));
-    val fixed = the_locale thy target |> #params |> #1 |> map #1;
+    val fixed = the_locale thy target |> #params |> map #1;
     val ((all_ids, syn), raw_elemss) = flatten (ctxt, intern_expr thy)
         ((raw_target_ids, target_syn), Expr expr);
     val (target_ids, ids) = chop (length raw_target_ids) all_ids;
     val ((parms, elemss, _), _) = read_elemss false ctxt fixed raw_elemss [];