# HG changeset patch
# User wenzelm
# Date 1427661498 -7200
# Node ID c5c4a936357acdb45e2dbe5891a06af5c4e8e948
# Parent  ab828c2c5d6759d6f2674fb25cf28f97363516d3# Parent  c7b7bca8592cf84846198346f5a37162ceeb7b23
merged

diff -r ab828c2c5d67 -r c5c4a936357a NEWS
--- a/NEWS	Sat Mar 28 21:32:48 2015 +0100
+++ b/NEWS	Sun Mar 29 22:38:18 2015 +0200
@@ -61,15 +61,19 @@
 
 *** Pure ***
 
-* Proof methods with explicit instantiation ("rule_tac", "subgoal_tac"
-etc.) allow an optional context of local variables ('for' declaration):
-these variables become schematic in the instantiated theorem. This
-behaviour is analogous to 'for' in attributes "where" and "of".
-
 * Explicit instantiation via attributes "where", "of", and proof methods
 "rule_tac" with derivatives like "subgoal_tac" etc. admit dummy patterns
 ("_") that stand for anonymous local variables.
 
+* Proof methods with explicit instantiation ("rule_tac", "subgoal_tac"
+etc.) allow an optional context of local variables ('for' declaration):
+these variables become schematic in the instantiated theorem; this
+behaviour is analogous to 'for' in attributes "where" and "of".
+Configuration option rule_insts_schematic (default false) controls use
+of schematic variables outside the context. Minor INCOMPATIBILITY,
+declare rule_insts_schematic = true temporarily and update to use local
+variable declarations or dummy patterns instead.
+
 * Configuration option "rule_insts_schematic" determines whether proof
 methods like "rule_tac" may refer to undeclared schematic variables
 implicitly, instead of using proper 'for' declarations.  This historic
diff -r ab828c2c5d67 -r c5c4a936357a src/Doc/Isar_Ref/HOL_Specific.thy
--- a/src/Doc/Isar_Ref/HOL_Specific.thy	Sat Mar 28 21:32:48 2015 +0100
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Sun Mar 29 22:38:18 2015 +0200
@@ -2338,7 +2338,7 @@
     ;
     @@{method (HOL) induct_tac} @{syntax goal_spec}? (@{syntax insts} * @'and') rule?
     ;
-    @@{method (HOL) ind_cases} (@{syntax prop}+) (@'for' (@{syntax name}+))?
+    @@{method (HOL) ind_cases} (@{syntax prop}+) @{syntax for_fixes}
     ;
     @@{command (HOL) inductive_cases} (@{syntax thmdecl}? (@{syntax prop}+) + @'and')
     ;
diff -r ab828c2c5d67 -r c5c4a936357a src/HOL/Codegenerator_Test/Candidates.thy
--- a/src/HOL/Codegenerator_Test/Candidates.thy	Sat Mar 28 21:32:48 2015 +0100
+++ b/src/HOL/Codegenerator_Test/Candidates.thy	Sun Mar 29 22:38:18 2015 +0200
@@ -13,11 +13,12 @@
 begin
 
 setup \<open>
+fn thy =>
 let
-  val tycos = (#log_types o Type.rep_tsig o Sign.tsig_of) @{theory};
-  val consts = map_filter (try (curry (Axclass.param_of_inst @{theory})
+  val tycos = Sign.logical_types thy;
+  val consts = map_filter (try (curry (Axclass.param_of_inst thy)
     @{const_name "Quickcheck_Narrowing.partial_term_of"})) tycos;
-in fold Code.del_eqns consts end
+in fold Code.del_eqns consts thy end
 \<close> -- \<open>drop technical stuff from @{text Quickcheck_Narrowing} which is tailored towards Haskell\<close>
 
 inductive sublist :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
diff -r ab828c2c5d67 -r c5c4a936357a src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy
--- a/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy	Sat Mar 28 21:32:48 2015 +0100
+++ b/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy	Sun Mar 29 22:38:18 2015 +0200
@@ -12,11 +12,12 @@
 begin
 
 setup \<open>
+fn thy =>
 let
-  val tycos = (#log_types o Type.rep_tsig o Sign.tsig_of) @{theory};
-  val consts = map_filter (try (curry (Axclass.param_of_inst @{theory})
+  val tycos = Sign.logical_types thy;
+  val consts = map_filter (try (curry (Axclass.param_of_inst thy)
     @{const_name "Quickcheck_Narrowing.partial_term_of"})) tycos;
-in fold Code.del_eqns consts end
+in fold Code.del_eqns consts thy end
 \<close> -- \<open>drop technical stuff from @{text Quickcheck_Narrowing} which is tailored towards Haskell\<close>
 
 (* 
diff -r ab828c2c5d67 -r c5c4a936357a src/HOL/Probability/measurable.ML
--- a/src/HOL/Probability/measurable.ML	Sat Mar 28 21:32:48 2015 +0100
+++ b/src/HOL/Probability/measurable.ML	Sun Mar 29 22:38:18 2015 +0200
@@ -147,8 +147,9 @@
   | indep (Abs (_,_,t)) top bot = indep t (top + 1) (bot + 1)
   | indep _ _ _ = true;
 
-fun cnt_prefixes ctxt (Abs (n, T, t)) = let
-      fun is_countable t = Type.of_sort (Proof_Context.tsig_of ctxt) (t, @{sort countable})
+fun cnt_prefixes ctxt (Abs (n, T, t)) =
+    let
+      fun is_countable ty = Sign.of_sort (Proof_Context.theory_of ctxt) (ty, @{sort countable})
       fun cnt_walk (Abs (ns, T, t)) Ts =
           map (fn (t', t'') => (Abs (ns, T, t'), t'')) (cnt_walk t (T::Ts))
         | cnt_walk (f $ g) Ts = let
diff -r ab828c2c5d67 -r c5c4a936357a src/HOL/Tools/functor.ML
--- a/src/HOL/Tools/functor.ML	Sat Mar 28 21:32:48 2015 +0100
+++ b/src/HOL/Tools/functor.ML	Sun Mar 29 22:38:18 2015 +0200
@@ -41,8 +41,9 @@
 
 (* type analysis *)
 
-fun term_with_typ ctxt T t = Envir.subst_term_types
-  (Type.typ_match (Proof_Context.tsig_of ctxt) (fastype_of t, T) Vartab.empty) t;
+fun term_with_typ ctxt T t =
+  Envir.subst_term_types
+    (Sign.typ_match (Proof_Context.theory_of ctxt) (fastype_of t, T) Vartab.empty) t;
 
 fun find_atomic ctxt T =
   let
diff -r ab828c2c5d67 -r c5c4a936357a src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Sat Mar 28 21:32:48 2015 +0100
+++ b/src/HOL/Tools/inductive.ML	Sun Mar 29 22:38:18 2015 +0200
@@ -38,6 +38,8 @@
     (string * thm list) list * local_theory
   val inductive_cases_i: (Attrib.binding * term list) list -> local_theory ->
     (string * thm list) list * local_theory
+  val ind_cases_rules: Proof.context ->
+    string list -> (binding * string option * mixfix) list -> thm list
   val inductive_simps: (Attrib.binding * string list) list -> local_theory ->
     (string * thm list) list * local_theory
   val inductive_simps_i: (Attrib.binding * term list) list -> local_theory ->
@@ -600,19 +602,22 @@
 val inductive_cases = gen_inductive_cases Attrib.check_src Syntax.read_prop;
 val inductive_cases_i = gen_inductive_cases (K I) Syntax.check_prop;
 
+
+(* ind_cases *)
+
+fun ind_cases_rules ctxt raw_props raw_fixes =
+  let
+    val (props, ctxt' ) = Specification.read_props raw_props raw_fixes ctxt;
+    val rules = Proof_Context.export ctxt' ctxt (map (mk_cases ctxt') props);
+  in rules end;
+
 val _ =
   Theory.setup
     (Method.setup @{binding ind_cases}
-      (Scan.lift (Scan.repeat1 Args.name_inner_syntax --
-        Scan.optional (Args.$$$ "for" |-- Scan.repeat1 Args.binding) []) >>
-        (fn (raw_props, fixes) => fn ctxt =>
-          let
-            val (_, ctxt') = Variable.add_fixes_binding fixes ctxt;
-            val props = Syntax.read_props ctxt' raw_props;
-            val ctxt'' = fold Variable.declare_term props ctxt';
-            val rules = Proof_Context.export ctxt'' ctxt (map (mk_cases ctxt'') props)
-          in Method.erule ctxt 0 rules end))
-      "dynamic case analysis on predicates");
+      (Scan.lift (Scan.repeat1 Parse.prop -- Parse.for_fixes) >>
+        (fn (props, fixes) => fn ctxt =>
+          Method.erule ctxt 0 (ind_cases_rules ctxt props fixes)))
+      "case analysis for inductive definitions, based on simplified elimination rule");
 
 
 (* derivation of simplified equation *)
diff -r ab828c2c5d67 -r c5c4a936357a src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Sat Mar 28 21:32:48 2015 +0100
+++ b/src/Pure/Isar/element.ML	Sun Mar 29 22:38:18 2015 +0200
@@ -236,7 +236,7 @@
     val concl_term = Object_Logic.drop_judgment thy concl;
 
     val fixes = fold_aterms (fn v as Free (x, T) =>
-        if Variable.newly_fixed ctxt' ctxt x andalso not (v aconv concl_term)
+        if Variable.is_newly_fixed ctxt' ctxt x andalso not (v aconv concl_term)
         then insert (op =) (Variable.revert_fixed ctxt' x, T) else I | _ => I) prop [] |> rev;
     val (assumes, cases) = take_suffix (fn prem =>
       is_elim andalso concl aconv Logic.strip_assums_concl prem) prems;
diff -r ab828c2c5d67 -r c5c4a936357a src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sat Mar 28 21:32:48 2015 +0100
+++ b/src/Pure/Isar/proof_context.ML	Sun Mar 29 22:38:18 2015 +0200
@@ -26,6 +26,7 @@
   val tsig_of: Proof.context -> Type.tsig
   val set_defsort: sort -> Proof.context -> Proof.context
   val default_sort: Proof.context -> indexname -> sort
+  val arity_sorts: Proof.context -> string -> sort -> sort list
   val consts_of: Proof.context -> Consts.T
   val set_syntax_mode: Syntax.mode -> Proof.context -> Proof.context
   val restore_syntax_mode: Proof.context -> Proof.context -> Proof.context
@@ -289,6 +290,7 @@
 val tsig_of = #1 o #tsig o rep_data;
 val set_defsort = map_tsig o apfst o Type.set_defsort;
 fun default_sort ctxt = the_default (Type.defaultS (tsig_of ctxt)) o Variable.def_sort ctxt;
+fun arity_sorts ctxt = Type.arity_sorts (Context.pretty ctxt) (tsig_of ctxt);
 
 val consts_of = #1 o #consts o rep_data;
 val cases_of = #cases o rep_data;
diff -r ab828c2c5d67 -r c5c4a936357a src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Sat Mar 28 21:32:48 2015 +0100
+++ b/src/Pure/Isar/specification.ML	Sun Mar 29 22:38:18 2015 +0200
@@ -7,6 +7,10 @@
 
 signature SPECIFICATION =
 sig
+  val read_props: string list -> (binding * string option * mixfix) list -> Proof.context ->
+    term list * Proof.context
+  val read_prop: string -> (binding * string option * mixfix) list -> Proof.context ->
+    term * Proof.context
   val check_spec:
     (binding * typ option * mixfix) list -> (Attrib.binding * term) list -> Proof.context ->
     (((binding * typ) * mixfix) list * (Attrib.binding * term) list) * Proof.context
@@ -79,6 +83,22 @@
 structure Specification: SPECIFICATION =
 struct
 
+(* prepare propositions *)
+
+fun read_props raw_props raw_fixes ctxt =
+  let
+    val ctxt1 = ctxt |> Proof_Context.read_vars raw_fixes |-> Proof_Context.add_fixes |> #2;
+    val props1 = map (Syntax.parse_prop ctxt1) raw_props;
+    val (props2, ctxt2) = ctxt1 |> fold_map Variable.fix_dummy_patterns props1;
+    val props3 = Syntax.check_props ctxt2 props2;
+    val ctxt3 = ctxt2 |> fold Variable.declare_term props3;
+  in (props3, ctxt3) end;
+
+fun read_prop raw_prop raw_fixes ctxt =
+  let val ([prop], ctxt') = read_props [raw_prop] raw_fixes ctxt
+  in (prop, ctxt') end;
+
+
 (* prepare specification *)
 
 local
diff -r ab828c2c5d67 -r c5c4a936357a src/Pure/Syntax/local_syntax.ML
--- a/src/Pure/Syntax/local_syntax.ML	Sat Mar 28 21:32:48 2015 +0100
+++ b/src/Pure/Syntax/local_syntax.ML	Sun Mar 29 22:38:18 2015 +0200
@@ -55,7 +55,7 @@
     val thy_syntax = Sign.syn_of thy;
     fun update_gram ((true, add, m), decls) = Syntax.update_type_gram add m decls
       | update_gram ((false, add, m), decls) =
-          Syntax.update_const_gram add (Sign.is_logtype thy) m decls;
+          Syntax.update_const_gram add (Sign.logical_types thy) m decls;
 
     val local_syntax = thy_syntax
       |> fold update_gram (AList.coalesce (op =) (rev (map snd mixfixes)));
diff -r ab828c2c5d67 -r c5c4a936357a src/Pure/Syntax/mixfix.ML
--- a/src/Pure/Syntax/mixfix.ML	Sat Mar 28 21:32:48 2015 +0100
+++ b/src/Pure/Syntax/mixfix.ML	Sun Mar 29 22:38:18 2015 +0200
@@ -26,7 +26,7 @@
   val make_type: int -> typ
   val binder_name: string -> string
   val syn_ext_types: (string * typ * mixfix) list -> Syntax_Ext.syn_ext
-  val syn_ext_consts: (string -> bool) -> (string * typ * mixfix) list -> Syntax_Ext.syn_ext
+  val syn_ext_consts: string list -> (string * typ * mixfix) list -> Syntax_Ext.syn_ext
 end;
 
 structure Mixfix: MIXFIX =
@@ -119,7 +119,7 @@
 val binder_stamp = stamp ();
 val binder_name = suffix "_binder";
 
-fun syn_ext_consts is_logtype const_decls =
+fun syn_ext_consts logical_types const_decls =
   let
     fun mk_infix sy ty c p1 p2 p3 =
       [Syntax_Ext.Mfix ("op " ^ sy, ty, c, [], 1000),
@@ -152,7 +152,7 @@
 
     val consts = binders @ map (fn (c, _, _) => (c, "")) const_decls;
   in
-    Syntax_Ext.syn_ext' is_logtype mfix consts ([], binder_trs, binder_trs', []) ([], [])
+    Syntax_Ext.syn_ext' logical_types mfix consts ([], binder_trs, binder_trs', []) ([], [])
   end;
 
 end;
diff -r ab828c2c5d67 -r c5c4a936357a src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Sat Mar 28 21:32:48 2015 +0100
+++ b/src/Pure/Syntax/syntax.ML	Sun Mar 29 22:38:18 2015 +0200
@@ -108,7 +108,7 @@
     (string * ((Proof.context -> typ -> term list -> term) * stamp)) list *
     (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list -> syntax -> syntax
   val update_type_gram: bool -> mode -> (string * typ * mixfix) list -> syntax -> syntax
-  val update_const_gram: bool -> (string -> bool) ->
+  val update_const_gram: bool -> string list ->
     mode -> (string * typ * mixfix) list -> syntax -> syntax
   val update_trrules: Ast.ast trrule list -> syntax -> syntax
   val remove_trrules: Ast.ast trrule list -> syntax -> syntax
@@ -659,8 +659,8 @@
 fun update_type_gram add prmode decls =
   (if add then update_syntax else remove_syntax) prmode (Mixfix.syn_ext_types decls);
 
-fun update_const_gram add is_logtype prmode decls =
-  (if add then update_syntax else remove_syntax) prmode (Mixfix.syn_ext_consts is_logtype decls);
+fun update_const_gram add logical_types prmode decls =
+  (if add then update_syntax else remove_syntax) prmode (Mixfix.syn_ext_consts logical_types decls);
 
 val update_trrules = update_syntax mode_default o Syntax_Ext.syn_ext_rules o check_rules;
 val remove_trrules = remove_syntax mode_default o Syntax_Ext.syn_ext_rules o check_rules;
diff -r ab828c2c5d67 -r c5c4a936357a src/Pure/Syntax/syntax_ext.ML
--- a/src/Pure/Syntax/syntax_ext.ML	Sat Mar 28 21:32:48 2015 +0100
+++ b/src/Pure/Syntax/syntax_ext.ML	Sun Mar 29 22:38:18 2015 +0200
@@ -31,7 +31,7 @@
   val mfix_delims: string -> string list
   val mfix_args: string -> int
   val escape: string -> string
-  val syn_ext': (string -> bool) -> mfix list ->
+  val syn_ext': string list -> mfix list ->
     (string * string) list -> (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list *
     (string * ((Proof.context -> term list -> term) * stamp)) list *
     (string * ((Proof.context -> typ -> term list -> term) * stamp)) list *
@@ -184,8 +184,10 @@
 
 (* mfix_to_xprod *)
 
-fun mfix_to_xprod is_logtype (mfix as Mfix (sy, typ, const, pris, pri)) =
+fun mfix_to_xprod logical_types (mfix as Mfix (sy, typ, const, pris, pri)) =
   let
+    val is_logtype = member (op =) logical_types;
+
     fun check_pri p =
       if p >= 0 andalso p <= 1000 then ()
       else err_in_mfix ("Precedence out of range: " ^ string_of_int p) mfix;
@@ -288,12 +290,12 @@
 
 (* syn_ext *)
 
-fun syn_ext' is_logtype mfixes consts trfuns (parse_rules, print_rules) =
+fun syn_ext' logical_types mfixes consts trfuns (parse_rules, print_rules) =
   let
     val (parse_ast_translation, parse_translation, print_translation,
       print_ast_translation) = trfuns;
 
-    val xprod_results = map (mfix_to_xprod is_logtype) mfixes;
+    val xprod_results = map (mfix_to_xprod logical_types) mfixes;
     val xprods = map #1 xprod_results;
     val consts' = map_filter #2 xprod_results;
     val parse_rules' = rev (map_filter #3 xprod_results);
@@ -311,7 +313,7 @@
   end;
 
 
-val syn_ext = syn_ext' (K false);
+val syn_ext = syn_ext' [];
 
 fun syn_ext_rules rules = syn_ext [] [] ([], [], [], []) rules;
 fun syn_ext_trfuns trfuns = syn_ext [] [] trfuns ([], []);
diff -r ab828c2c5d67 -r c5c4a936357a src/Pure/Tools/rule_insts.ML
--- a/src/Pure/Tools/rule_insts.ML	Sat Mar 28 21:32:48 2015 +0100
+++ b/src/Pure/Tools/rule_insts.ML	Sun Mar 29 22:38:18 2015 +0200
@@ -92,7 +92,7 @@
       |> Syntax.check_terms ctxt'
       |> Variable.polymorphic ctxt';
     val Ts' = map Term.fastype_of ts';
-    val tyenv = fold Type.raw_match (Ts ~~ Ts') Vartab.empty;
+    val tyenv = fold (Sign.typ_match (Proof_Context.theory_of ctxt)) (Ts ~~ Ts') Vartab.empty;
     val tyenv' = Vartab.fold (fn (xi, (S, T)) => cons ((xi, S), T)) tyenv [];
   in ((ts', tyenv'), ctxt') end;
 
@@ -209,7 +209,8 @@
 
 (* goal context *)
 
-val schematic = Attrib.setup_config_bool @{binding rule_insts_schematic} (K true);
+(*legacy*)
+val schematic = Attrib.setup_config_bool @{binding rule_insts_schematic} (K false);
 
 fun goal_context goal ctxt =
   let
@@ -228,29 +229,24 @@
   let
     (* goal context *)
 
-    val (params, param_ctxt) = goal_context (Thm.term_of cgoal) ctxt;
+    val (params, goal_ctxt) = goal_context (Thm.term_of cgoal) ctxt;
     val paramTs = map #2 params;
 
 
-    (* local fixes *)
-
-    val fixes_ctxt = param_ctxt
-      |> Proof_Context.read_vars fixes |-> Proof_Context.add_fixes |> #2;
+    (* instantiation context *)
 
-    val ((inst_tvars, inst_vars), inst_ctxt) = read_insts thm mixed_insts fixes_ctxt;
+    val ((inst_tvars, inst_vars), inst_ctxt) = goal_ctxt
+      |> Proof_Context.read_vars fixes |-> Proof_Context.add_fixes |> #2
+      |> read_insts thm mixed_insts;
 
-    fun add_fixed (Free (x, _)) =
-          if Variable.newly_fixed inst_ctxt param_ctxt x
-          then insert (op =) x else I
-      | add_fixed _ = I;
-    val fixed = fold (Term.fold_aterms add_fixed o #2) inst_vars [];
+    val fixed = map #1 (fold (Variable.add_newly_fixed inst_ctxt goal_ctxt o #2) inst_vars []);
 
 
     (* lift and instantiate rule *)
 
     val inc = Thm.maxidx_of st + 1;
     val lift_type = Logic.incr_tvar inc;
-    fun lift_var ((a, j), T) = Var ((a, j + inc), paramTs ---> Logic.incr_tvar inc T);
+    fun lift_var ((a, j), T) = Var ((a, j + inc), paramTs ---> lift_type T);
     fun lift_term t = fold_rev Term.absfree params (Logic.incr_indexes (fixed, paramTs, inc) t);
 
     val inst_tvars' = inst_tvars
@@ -260,10 +256,8 @@
 
     val thm' = Thm.lift_rule cgoal thm
       |> Drule.instantiate_normalize (inst_tvars', inst_vars')
-      |> singleton (Variable.export inst_ctxt param_ctxt);
-  in
-    compose_tac param_ctxt (bires_flag, thm', Thm.nprems_of thm) i
-  end) i st;
+      |> singleton (Variable.export inst_ctxt ctxt);
+  in compose_tac ctxt (bires_flag, thm', Thm.nprems_of thm) i end) i st;
 
 val res_inst_tac = bires_inst_tac false;
 val eres_inst_tac = bires_inst_tac true;
diff -r ab828c2c5d67 -r c5c4a936357a src/Pure/sign.ML
--- a/src/Pure/sign.ML	Sat Mar 28 21:32:48 2015 +0100
+++ b/src/Pure/sign.ML	Sun Mar 29 22:38:18 2015 +0200
@@ -24,7 +24,7 @@
   val of_sort: theory -> typ * sort -> bool
   val inter_sort: theory -> sort * sort -> sort
   val witness_sorts: theory -> (typ * sort) list -> sort list -> (typ * sort) list
-  val is_logtype: theory -> string -> bool
+  val logical_types: theory -> string list
   val typ_instance: theory -> typ * typ -> bool
   val typ_equiv: theory -> typ * typ -> bool
   val typ_match: theory -> typ * typ -> Type.tyenv -> Type.tyenv
@@ -190,7 +190,7 @@
 val of_sort = Type.of_sort o tsig_of;
 val inter_sort = Type.inter_sort o tsig_of;
 val witness_sorts = Type.witness_sorts o tsig_of;
-val is_logtype = member (op =) o Type.logical_types o tsig_of;
+val logical_types = Type.logical_types o tsig_of;
 
 val typ_instance = Type.typ_instance o tsig_of;
 fun typ_equiv thy (T, U) = typ_instance thy (T, U) andalso typ_instance thy (U, T);
@@ -369,7 +369,7 @@
     val ctxt = Type.set_mode Type.mode_syntax (Proof_Context.init_global thy);
     fun prep (c, T, mx) = (c, certify_typ_mode Type.mode_syntax thy (parse_typ ctxt T), mx)
       handle ERROR msg => cat_error msg ("in syntax declaration " ^ quote c);
-  in thy |> map_syn (change_gram (is_logtype thy) mode (map prep args)) end;
+  in thy |> map_syn (change_gram (logical_types thy) mode (map prep args)) end;
 
 fun gen_add_syntax x = gen_syntax (Syntax.update_const_gram true) x;
 
diff -r ab828c2c5d67 -r c5c4a936357a src/Pure/type.ML
--- a/src/Pure/type.ML	Sat Mar 28 21:32:48 2015 +0100
+++ b/src/Pure/type.ML	Sun Mar 29 22:38:18 2015 +0200
@@ -49,7 +49,6 @@
   val restore_mode: Proof.context -> Proof.context -> Proof.context
   val type_space: tsig -> Name_Space.T
   val type_alias: Name_Space.naming -> binding -> string -> tsig -> tsig
-  val is_logtype: tsig -> string -> bool
   val check_decl: Context.generic -> tsig ->
     xstring * Position.T -> (string * Position.report list) * decl
   val the_decl: tsig -> string * Position.T -> decl
@@ -252,8 +251,6 @@
 fun type_alias naming binding name = map_tsig (fn (classes, default, types) =>
   (classes, default, (Name_Space.alias_table naming binding name types)));
 
-val is_logtype = member (op =) o logical_types;
-
 
 fun undecl_type c = "Undeclared type constructor: " ^ quote c;
 
diff -r ab828c2c5d67 -r c5c4a936357a src/Pure/type_infer_context.ML
--- a/src/Pure/type_infer_context.ML	Sat Mar 28 21:32:48 2015 +0100
+++ b/src/Pure/type_infer_context.ML	Sun Mar 29 22:38:18 2015 +0200
@@ -169,7 +169,7 @@
 fun unify ctxt =
   let
     val thy = Proof_Context.theory_of ctxt;
-    val arity_sorts = Type.arity_sorts (Context.pretty ctxt) (Sign.tsig_of thy);
+    val arity_sorts = Proof_Context.arity_sorts ctxt;
 
 
     (* adjust sorts of parameters *)
diff -r ab828c2c5d67 -r c5c4a936357a src/Pure/variable.ML
--- a/src/Pure/variable.ML	Sat Mar 28 21:32:48 2015 +0100
+++ b/src/Pure/variable.ML	Sun Mar 29 22:38:18 2015 +0200
@@ -38,7 +38,7 @@
   val restore_proper_fixes: Proof.context -> Proof.context -> Proof.context
   val is_improper: Proof.context -> string -> bool
   val is_fixed: Proof.context -> string -> bool
-  val newly_fixed: Proof.context -> Proof.context -> string -> bool
+  val is_newly_fixed: Proof.context -> Proof.context -> string -> bool
   val fixed_ord: Proof.context -> string * string -> order
   val intern_fixed: Proof.context -> string -> string
   val markup_fixed: Proof.context -> string -> Markup.T
@@ -46,6 +46,8 @@
   val revert_fixed: Proof.context -> string -> string
   val add_fixed_names: Proof.context -> term -> string list -> string list
   val add_fixed: Proof.context -> term -> (string * typ) list -> (string * typ) list
+  val add_newly_fixed: Proof.context -> Proof.context ->
+    term -> (string * typ) list -> (string * typ) list
   val add_free_names: Proof.context -> term -> string list -> string list
   val add_frees: Proof.context -> term -> (string * typ) list -> (string * typ) list
   val add_fixes_binding: binding list -> Proof.context -> string list * Proof.context
@@ -346,7 +348,7 @@
 (* specialized name space *)
 
 val is_fixed = Name_Space.defined_entry o fixes_space;
-fun newly_fixed inner outer = is_fixed inner andf (not o is_fixed outer);
+fun is_newly_fixed inner outer = is_fixed inner andf (not o is_fixed outer);
 
 val fixed_ord = Name_Space.entry_ord o fixes_space;
 val intern_fixed = Name_Space.intern o fixes_space;
@@ -383,6 +385,9 @@
 fun add_fixed ctxt =
   fold_aterms (fn Free (x, T) => is_fixed ctxt x ? insert (op =) (x, T) | _ => I);
 
+fun add_newly_fixed ctxt' ctxt =
+  fold_aterms (fn Free (x, T) => is_newly_fixed ctxt' ctxt x ? insert (op =) (x, T) | _ => I);
+
 
 (* declarations *)
 
@@ -474,7 +479,7 @@
 fun export_inst inner outer =
   let
     val declared_outer = is_declared outer;
-    val still_fixed = not o newly_fixed inner outer;
+    val still_fixed = not o is_newly_fixed inner outer;
 
     val gen_fixes =
       Name_Space.fold_table (fn (y, _) => not (is_fixed outer y) ? cons y)
diff -r ab828c2c5d67 -r c5c4a936357a src/Tools/Code/code_preproc.ML
--- a/src/Tools/Code/code_preproc.ML	Sat Mar 28 21:32:48 2015 +0100
+++ b/src/Tools/Code/code_preproc.ML	Sun Mar 29 22:38:18 2015 +0200
@@ -371,8 +371,9 @@
         val thy = Proof_Context.theory_of ctxt;
         val all_classes = complete_proper_sort thy [class];
         val super_classes = remove (op =) class all_classes;
-        val classess = map (complete_proper_sort thy)
-          (Sign.arity_sorts thy tyco [class]);
+        val classess =
+          map (complete_proper_sort thy)
+            (Proof_Context.arity_sorts ctxt tyco [class]);
         val inst_params = inst_params thy tyco all_classes;
       in (classess, (super_classes, inst_params)) end;
 
@@ -410,7 +411,7 @@
     |> apfst (Vargraph.add_edge (c_k, c_k'))
   end
 and ensure_typmatch_inst ctxt arities eqngr (tyco, styps) class vardeps_data =
-  if can (Sign.arity_sorts (Proof_Context.theory_of ctxt) tyco) [class]
+  if can (Proof_Context.arity_sorts ctxt tyco) [class]
   then vardeps_data
     |> ensure_inst ctxt arities eqngr (class, tyco)
     |> fold_index (fn (k, styp) =>
diff -r ab828c2c5d67 -r c5c4a936357a src/Tools/induct.ML
--- a/src/Tools/induct.ML	Sat Mar 28 21:32:48 2015 +0100
+++ b/src/Tools/induct.ML	Sun Mar 29 22:38:18 2015 +0200
@@ -394,12 +394,11 @@
 
 fun prep_inst ctxt align tune (tm, ts) =
   let
-    val cert = Thm.global_cterm_of (Proof_Context.theory_of ctxt);
     fun prep_var (x, SOME t) =
           let
-            val cx = cert x;
+            val cx = Thm.cterm_of ctxt x;
             val xT = Thm.typ_of_cterm cx;
-            val ct = cert (tune t);
+            val ct = Thm.cterm_of ctxt (tune t);
             val tT = Thm.typ_of_cterm ct;
           in
             if Type.could_unify (tT, xT) then SOME (cx, ct)
@@ -478,8 +477,6 @@
 
 fun cases_tac ctxt simp insts opt_rule facts =
   let
-    val thy = Proof_Context.theory_of ctxt;
-
     fun inst_rule r =
       (if null insts then r
        else
@@ -505,7 +502,7 @@
           val rule' = rule
             |> simp ? (simplified_rule' ctxt #> unmark_constraints ctxt);
         in
-          CASES (Rule_Cases.make_common (thy,
+          CASES (Rule_Cases.make_common (Proof_Context.theory_of ctxt,
               Thm.prop_of (Rule_Cases.internalize_params rule')) cases)
             ((Method.insert_tac more_facts THEN' resolve_tac ctxt [rule'] THEN_ALL_NEW
                 (if simp then TRY o trivial_tac ctxt else K all_tac)) i) st
@@ -569,21 +566,18 @@
 
 local
 
-fun dest_env thy env =
+fun dest_env ctxt env =
   let
-    val cert = Thm.global_cterm_of thy;
-    val certT = Thm.global_ctyp_of thy;
     val pairs = Vartab.dest (Envir.term_env env);
     val types = Vartab.dest (Envir.type_env env);
-    val ts = map (cert o Envir.norm_term env o #2 o #2) pairs;
-    val xs = map2 (curry (cert o Var)) (map #1 pairs) (map Thm.typ_of_cterm ts);
-  in (map (fn (xi, (S, T)) => (certT (TVar (xi, S)), certT T)) types, xs ~~ ts) end;
+    val ts = map (Thm.cterm_of ctxt o Envir.norm_term env o #2 o #2) pairs;
+    val xs = map2 (curry (Thm.cterm_of ctxt o Var)) (map #1 pairs) (map Thm.typ_of_cterm ts);
+  in (map (fn (xi, (S, T)) => apply2 (Thm.ctyp_of ctxt) (TVar (xi, S), T)) types, xs ~~ ts) end;
 
 in
 
 fun guess_instance ctxt rule i st =
   let
-    val thy = Proof_Context.theory_of ctxt;
     val maxidx = Thm.maxidx_of st;
     val goal = Thm.term_of (Thm.cprem_of st i);  (*exception Subscript*)
     val params = rev (Term.rename_wrt_term goal (Logic.strip_params goal));
@@ -599,7 +593,7 @@
       in
         Unify.smash_unifiers (Context.Proof ctxt)
           [(Thm.concl_of rule', concl)] (Envir.empty (Thm.maxidx_of rule'))
-        |> Seq.map (fn env => Drule.instantiate_normalize (dest_env thy env) rule')
+        |> Seq.map (fn env => Drule.instantiate_normalize (dest_env ctxt env) rule')
       end
   end
   handle General.Subscript => Seq.empty;
@@ -654,19 +648,17 @@
 
 fun meta_spec_tac ctxt n (x, T) = SUBGOAL (fn (goal, i) =>
   let
-    val thy = Proof_Context.theory_of ctxt;
-    val cert = Thm.global_cterm_of thy;
-
     val v = Free (x, T);
     fun spec_rule prfx (xs, body) =
       @{thm Pure.meta_spec}
       |> Thm.rename_params_rule ([Name.clean (Variable.revert_fixed ctxt x)], 1)
-      |> Thm.lift_rule (cert prfx)
+      |> Thm.lift_rule (Thm.cterm_of ctxt prfx)
       |> `(Thm.prop_of #> Logic.strip_assums_concl)
       |-> (fn pred $ arg =>
         Drule.cterm_instantiate
-          [(cert (Term.head_of pred), cert (Logic.rlist_abs (xs, body))),
-           (cert (Term.head_of arg), cert (Logic.rlist_abs (xs, v)))]);
+          (map (apply2 (Thm.cterm_of ctxt))
+            [(Term.head_of pred, Logic.rlist_abs (xs, body)),
+             (Term.head_of arg, Logic.rlist_abs (xs, v))]));
 
     fun goal_concl k xs (Const (@{const_name Pure.all}, _) $ Abs (a, T, B)) =
           goal_concl k ((a, T) :: xs) B
@@ -835,8 +827,6 @@
 
 fun coinduct_tac ctxt inst taking opt_rule facts = SUBGOAL_CASES (fn (goal, i, st) =>
   let
-    val thy = Proof_Context.theory_of ctxt;
-
     fun inst_rule r =
       if null inst then `Rule_Cases.get r
       else Drule.cterm_instantiate (prep_inst ctxt align_right I (main_prop_of r, inst)) r
@@ -857,7 +847,7 @@
         guess_instance ctxt rule i st
         |> Seq.map (rule_instance ctxt (burrow_options (Variable.polymorphic ctxt) taking))
         |> Seq.maps (fn rule' =>
-          CASES (Rule_Cases.make_common (thy,
+          CASES (Rule_Cases.make_common (Proof_Context.theory_of ctxt,
               Thm.prop_of (Rule_Cases.internalize_params rule')) cases)
             (Method.insert_tac more_facts i THEN resolve_tac ctxt [rule'] i) st))
   end);
diff -r ab828c2c5d67 -r c5c4a936357a src/Tools/subtyping.ML
--- a/src/Tools/subtyping.ML	Sat Mar 28 21:32:48 2015 +0100
+++ b/src/Tools/subtyping.ML	Sun Mar 29 22:38:18 2015 +0200
@@ -144,7 +144,7 @@
 fun unify weak ctxt =
   let
     val thy = Proof_Context.theory_of ctxt;
-    val arity_sorts = Type.arity_sorts (Context.pretty ctxt) (Sign.tsig_of thy);
+    val arity_sorts = Proof_Context.arity_sorts ctxt;
 
 
     (* adjust sorts of parameters *)
@@ -344,7 +344,7 @@
 
     val coes_graph = coes_graph_of ctxt;
     val tmaps = tmaps_of ctxt;
-    val arity_sorts = Type.arity_sorts (Context.pretty ctxt) (Sign.tsig_of thy);
+    val arity_sorts = Proof_Context.arity_sorts ctxt;
 
     fun split_cs _ [] = ([], [])
       | split_cs f (c :: cs) =