--- a/src/HOL/Statespace/state_fun.ML Thu Apr 15 16:55:12 2010 +0200
+++ b/src/HOL/Statespace/state_fun.ML Thu Apr 15 18:13:25 2010 +0200
@@ -193,7 +193,7 @@
(* mk_updterm returns
* - (orig-term-skeleton,simplified-term-skeleton, vars, b)
- * where boolean b tells if a simplification has occured.
+ * where boolean b tells if a simplification has occurred.
"orig-term-skeleton = simplified-term-skeleton" is
* the desired simplification rule.
* The algorithm first walks down the updates to the seed-state while
--- a/src/HOL/Statespace/state_space.ML Thu Apr 15 16:55:12 2010 +0200
+++ b/src/HOL/Statespace/state_space.ML Thu Apr 15 18:13:25 2010 +0200
@@ -478,6 +478,21 @@
Type (name, Ts) => (Ts, name)
| T => error ("Bad parent statespace specification: " ^ Syntax.string_of_typ ctxt T));
+fun read_typ ctxt raw_T env =
+ let
+ val ctxt' = fold (Variable.declare_typ o TFree) env ctxt;
+ val T = Syntax.read_typ ctxt' raw_T;
+ val env' = OldTerm.add_typ_tfrees (T, env);
+ in (T, env') end;
+
+fun cert_typ ctxt raw_T env =
+ let
+ val thy = ProofContext.theory_of ctxt;
+ val T = Type.no_tvars (Sign.certify_typ thy raw_T)
+ handle TYPE (msg, _, _) => error msg;
+ val env' = OldTerm.add_typ_tfrees (T, env);
+ in (T, env') end;
+
fun gen_define_statespace prep_typ state_space args name parents comps thy =
let (* - args distinct
- only args may occur in comps and parent-instantiations
@@ -500,7 +515,7 @@
val (Ts',env') = fold_map (prep_typ ctxt) Ts env
handle ERROR msg => cat_error msg
- ("The error(s) above occured in parent statespace specification "
+ ("The error(s) above occurred in parent statespace specification "
^ quote pname);
val err_insts = if length args <> length Ts' then
["number of type instantiation(s) does not match arguments of parent statespace "
@@ -539,7 +554,7 @@
fun prep_comp (n,T) env =
let val (T', env') = prep_typ ctxt T env handle ERROR msg =>
- cat_error msg ("The error(s) above occured in component " ^ quote n)
+ cat_error msg ("The error(s) above occurred in component " ^ quote n)
in ((n,T'), env') end;
val (comps',env') = fold_map prep_comp comps env;
@@ -579,8 +594,8 @@
end
handle ERROR msg => cat_error msg ("Failed to define statespace " ^ quote name);
-val define_statespace = gen_define_statespace Record.read_typ NONE;
-val define_statespace_i = gen_define_statespace Record.cert_typ;
+val define_statespace = gen_define_statespace read_typ NONE;
+val define_statespace_i = gen_define_statespace cert_typ;
(*** parse/print - translations ***)
--- a/src/HOL/Tools/Datatype/datatype.ML Thu Apr 15 16:55:12 2010 +0200
+++ b/src/HOL/Tools/Datatype/datatype.ML Thu Apr 15 18:13:25 2010 +0200
@@ -682,7 +682,7 @@
(constrs @ [(c, map (dtyp_of_typ new_dts) cargs')],
constr_syntax' @ [(cname, mx')], sorts'')
end handle ERROR msg => cat_error msg
- ("The error above occured in constructor " ^ quote (Binding.str_of cname) ^
+ ("The error above occurred in constructor " ^ quote (Binding.str_of cname) ^
" of datatype " ^ quote (Binding.str_of tname));
val (constrs', constr_syntax', sorts') =
--- a/src/HOL/Tools/record.ML Thu Apr 15 16:55:12 2010 +0200
+++ b/src/HOL/Tools/record.ML Thu Apr 15 18:13:25 2010 +0200
@@ -54,9 +54,9 @@
val print_records: theory -> unit
val read_typ: Proof.context -> string -> (string * sort) list -> typ * (string * sort) list
val cert_typ: Proof.context -> typ -> (string * sort) list -> typ * (string * sort) list
- val add_record: bool -> string list * binding -> (typ list * string) option ->
+ val add_record: bool -> (string * sort) list * binding -> (typ list * string) option ->
(binding * typ * mixfix) list -> theory -> theory
- val add_record_cmd: bool -> string list * binding -> string option ->
+ val add_record_cmd: bool -> (string * string option) list * binding -> string option ->
(binding * string * mixfix) list -> theory -> theory
val setup: theory -> theory
end;
@@ -64,7 +64,8 @@
signature ISO_TUPLE_SUPPORT =
sig
- val add_iso_tuple_type: bstring * string list -> typ * typ -> theory -> (term * term) * theory
+ val add_iso_tuple_type: bstring * (string * sort) list ->
+ typ * typ -> theory -> (term * term) * theory
val mk_cons_tuple: term * term -> term
val dest_cons_tuple: term -> term * term
val iso_tuple_intros_tac: int -> tactic
@@ -900,10 +901,9 @@
val midx = maxidx_of_typ T;
val varifyT = varifyT midx;
- fun mk_type_abbr subst name alphas =
- let val abbrT = Type (name, map (fn a => varifyT (TFree (a, HOLogic.typeS))) alphas) in
- Syntax.term_of_typ (! Syntax.show_sorts) (Envir.norm_type subst abbrT)
- end;
+ fun mk_type_abbr subst name args =
+ let val abbrT = Type (name, map (varifyT o TFree) args)
+ in Syntax.term_of_typ (! Syntax.show_sorts) (Envir.norm_type subst abbrT) end;
fun match rT T = Sign.typ_match thy (varifyT rT, T) Vartab.empty;
in
@@ -912,7 +912,7 @@
SOME (name, _) =>
if name = last_ext then
let val subst = match schemeT T in
- if HOLogic.is_unitT (Envir.norm_type subst (varifyT (TFree (zeta, HOLogic.typeS))))
+ if HOLogic.is_unitT (Envir.norm_type subst (varifyT (TFree zeta)))
then mk_type_abbr subst abbr alphas
else mk_type_abbr subst (suffix schemeN abbr) (alphas @ [zeta])
end handle Type.TYPE_MATCH => record_type_tr' ctxt tm
@@ -1639,11 +1639,10 @@
val fields_moreTs = fieldTs @ [moreT];
val alphas_zeta = alphas @ [zeta];
- val alphas_zetaTs = map (fn a => TFree (a, HOLogic.typeS)) alphas_zeta;
val ext_binding = Binding.name (suffix extN base_name);
val ext_name = suffix extN name;
- val extT = Type (suffix ext_typeN name, alphas_zetaTs);
+ val extT = Type (suffix ext_typeN name, map TFree alphas_zeta);
val ext_type = fields_moreTs ---> extT;
@@ -1846,10 +1845,8 @@
(* record_definition *)
-fun record_definition (args, binding) parent (parents: parent_info list) raw_fields thy =
+fun record_definition (alphas, binding) parent (parents: parent_info list) raw_fields thy =
let
- val alphas = map fst args;
-
val name = Sign.full_name thy binding;
val full = Sign.full_name_path thy (Binding.name_of binding); (* FIXME Binding.qualified (!?) *)
@@ -1869,7 +1866,7 @@
val fields = map (apfst full) bfields;
val names = map fst fields;
val types = map snd fields;
- val alphas_fields = fold Term.add_tfree_namesT types [];
+ val alphas_fields = fold Term.add_tfreesT types [];
val alphas_ext = inter (op =) alphas_fields alphas;
val len = length fields;
val variants =
@@ -1885,9 +1882,8 @@
val all_vars = parent_vars @ vars;
val all_named_vars = (parent_names ~~ parent_vars) @ named_vars;
-
- val zeta = Name.variant alphas "'z";
- val moreT = TFree (zeta, HOLogic.typeS);
+ val zeta = (Name.variant (map #1 alphas) "'z", HOLogic.typeS);
+ val moreT = TFree zeta;
val more = Free (moreN, moreT);
val full_moreN = full (Binding.name moreN);
val bfields_more = bfields @ [(Binding.name moreN, moreT)];
@@ -1978,8 +1974,8 @@
(*record (scheme) type abbreviation*)
val recordT_specs =
- [(Binding.suffix_name schemeN binding, alphas @ [zeta], rec_schemeT0, NoSyn),
- (binding, alphas, recT0, NoSyn)];
+ [(Binding.suffix_name schemeN binding, map #1 (alphas @ [zeta]), rec_schemeT0, NoSyn),
+ (binding, map #1 alphas, recT0, NoSyn)];
val ext_defs = ext_def :: map #ext_def parents;
@@ -2349,7 +2345,7 @@
((Binding.name "iffs", iffs), [iff_add])];
val info =
- make_record_info args parent fields extension
+ make_record_info alphas parent fields extension
ext_induct ext_inject ext_surjective ext_split ext_def
sel_convs' upd_convs' sel_defs' upd_defs' fold_congs' unfold_congs' splits' derived_defs'
surjective' equality' induct_scheme' induct' cases_scheme' cases' simps' iffs';
@@ -2371,10 +2367,25 @@
(* add_record *)
-(*We do all preparations and error checks here, deferring the real
- work to record_definition.*)
-fun gen_add_record prep_typ prep_raw_parent quiet_mode
- (params, binding) raw_parent raw_fields thy =
+local
+
+fun read_parent NONE ctxt = (NONE, ctxt)
+ | read_parent (SOME raw_T) ctxt =
+ (case ProofContext.read_typ_abbrev ctxt raw_T of
+ Type (name, Ts) => (SOME (Ts, name), fold Variable.declare_typ Ts ctxt)
+ | T => error ("Bad parent record specification: " ^ Syntax.string_of_typ ctxt T));
+
+fun prep_field prep (x, T, mx) = (x, prep T, mx)
+ handle ERROR msg =>
+ cat_error msg ("The error(s) above occurred in record field " ^ quote (Binding.str_of x));
+
+fun read_field raw_field ctxt =
+ let val field as (_, T, _) = prep_field (Syntax.read_typ ctxt) raw_field
+ in (field, Variable.declare_typ T ctxt) end;
+
+in
+
+fun add_record quiet_mode (params, binding) raw_parent raw_fields thy =
let
val _ = Theory.requires thy "Record" "record definitions";
val _ =
@@ -2382,40 +2393,19 @@
else writeln ("Defining record " ^ quote (Binding.str_of binding) ^ " ...");
val ctxt = ProofContext.init thy;
-
-
- (* parents *)
-
- fun prep_inst T = fst (cert_typ ctxt T []);
-
- val parent = Option.map (apfst (map prep_inst) o prep_raw_parent ctxt) raw_parent
- handle ERROR msg => cat_error msg ("The error(s) above in parent record specification");
+ fun cert_typ T = Type.no_tvars (ProofContext.cert_typ ctxt T)
+ handle TYPE (msg, _, _) => error msg;
+
+
+ (* specification *)
+
+ val parent = Option.map (apfst (map cert_typ)) raw_parent
+ handle ERROR msg =>
+ cat_error msg ("The error(s) above occurred in parent record specification");
+ val parent_args = (case parent of SOME (Ts, _) => Ts | NONE => []);
val parents = add_parents thy parent [];
- val init_env =
- (case parent of
- NONE => []
- | SOME (types, _) => fold Term.add_tfreesT types []);
-
-
- (* fields *)
-
- fun prep_field (x, raw_T, mx) env =
- let
- val (T, env') =
- prep_typ ctxt raw_T env handle ERROR msg =>
- cat_error msg ("The error(s) above occured in record field " ^ quote (Binding.str_of x));
- in ((x, T, mx), env') end;
-
- val (bfields, envir) = fold_map prep_field raw_fields init_env;
- val envir_names = map fst envir;
-
-
- (* args *)
-
- val defaultS = Sign.defaultS thy;
- val args = map (fn x => (x, AList.lookup (op =) envir x |> the_default defaultS)) params;
-
+ val bfields = map (prep_field cert_typ) raw_fields;
(* errors *)
@@ -2424,15 +2414,12 @@
if is_none (get_record thy name) then []
else ["Duplicate definition of record " ^ quote name];
- val err_dup_parms =
- (case duplicates (op =) params of
+ val spec_frees = fold Term.add_tfreesT (parent_args @ map #2 bfields) [];
+ val err_extra_frees =
+ (case subtract (op =) params spec_frees of
[] => []
- | dups => ["Duplicate parameter(s) " ^ commas dups]);
-
- val err_extra_frees =
- (case subtract (op =) params envir_names of
- [] => []
- | extras => ["Extra free type variable(s) " ^ commas extras]);
+ | extras => ["Extra free type variable(s) " ^
+ commas (map (Syntax.string_of_typ ctxt o TFree) extras)]);
val err_no_fields = if null bfields then ["No fields present"] else [];
@@ -2445,23 +2432,25 @@
if forall (not_equal moreN o Binding.name_of o #1) bfields then []
else ["Illegal field name " ^ quote moreN];
- val err_dup_sorts =
- (case duplicates (op =) envir_names of
- [] => []
- | dups => ["Inconsistent sort constraints for " ^ commas dups]);
-
val errs =
- err_dup_record @ err_dup_parms @ err_extra_frees @ err_no_fields @
- err_dup_fields @ err_bad_fields @ err_dup_sorts;
-
+ err_dup_record @ err_extra_frees @ err_no_fields @ err_dup_fields @ err_bad_fields;
val _ = if null errs then () else error (cat_lines errs);
in
- thy |> record_definition (args, binding) parent parents bfields
+ thy |> record_definition (params, binding) parent parents bfields
end
handle ERROR msg => cat_error msg ("Failed to define record " ^ quote (Binding.str_of binding));
-val add_record = gen_add_record cert_typ (K I);
-val add_record_cmd = gen_add_record read_typ read_raw_parent;
+fun add_record_cmd quiet_mode (raw_params, binding) raw_parent raw_fields thy =
+ let
+ val ctxt = ProofContext.init thy;
+ val params = map (apsnd (Typedecl.read_constraint ctxt)) raw_params;
+ val ctxt1 = fold (Variable.declare_typ o TFree) params ctxt;
+ val (parent, ctxt2) = read_parent raw_parent ctxt1;
+ val (fields, ctxt3) = fold_map read_field raw_fields ctxt2;
+ val params' = map (ProofContext.check_tfree ctxt3) params;
+ in thy |> add_record quiet_mode (params', binding) parent fields end;
+
+end;
(* setup theory *)
@@ -2479,7 +2468,7 @@
val _ =
OuterSyntax.command "record" "define extensible record" K.thy_decl
- (P.type_args -- P.binding --
+ (P.type_args_constrained -- P.binding --
(P.$$$ "=" |-- Scan.option (P.typ --| P.$$$ "+") -- Scan.repeat1 P.const_binding)
>> (fn (x, (y, z)) => Toplevel.theory (add_record_cmd false x y z)));
--- a/src/HOL/Tools/typecopy.ML Thu Apr 15 16:55:12 2010 +0200
+++ b/src/HOL/Tools/typecopy.ML Thu Apr 15 18:13:25 2010 +0200
@@ -8,7 +8,7 @@
sig
type info = { vs: (string * sort) list, constr: string, typ: typ,
inject: thm, proj: string * typ, proj_def: thm }
- val typecopy: binding * string list -> typ -> (binding * binding) option
+ val typecopy: binding * (string * sort) list -> typ -> (binding * binding) option
-> theory -> (string * info) * theory
val get_info: theory -> string -> info option
val interpretation: (string -> theory -> theory) -> theory -> theory
@@ -52,8 +52,9 @@
fun typecopy (raw_tyco, raw_vs) raw_ty constr_proj thy =
let
val ty = Sign.certify_typ thy raw_ty;
- val vs =
- AList.make (the_default HOLogic.typeS o AList.lookup (op =) (Term.add_tfreesT ty [])) raw_vs;
+ val ctxt = ProofContext.init thy |> Variable.declare_typ ty;
+ val vs = raw_vs |>
+ map (fn (a, S) => (a, if S = dummyS then ProofContext.default_sort ctxt (a, ~1) else S));
val tac = Tactic.rtac UNIV_witness 1;
fun add_info tyco (({ abs_type = ty_abs, rep_type = ty_rep, Abs_name = c_abs,
Rep_name = c_rep, ...}, { Abs_inject = inject, Abs_inverse = inverse, ... })
@@ -80,8 +81,7 @@
end
in
thy
- |> Typedef.add_typedef_global false (SOME raw_tyco)
- (raw_tyco, map (fn (v, _) => (v, dummyS)) vs, NoSyn) (* FIXME keep constraints!? *)
+ |> Typedef.add_typedef_global false (SOME raw_tyco) (raw_tyco, vs, NoSyn)
(HOLogic.mk_UNIV ty) (Option.map swap constr_proj) tac
|-> (fn (tyco, info) => add_info tyco info)
end;
--- a/src/HOL/Tools/typedef.ML Thu Apr 15 16:55:12 2010 +0200
+++ b/src/HOL/Tools/typedef.ML Thu Apr 15 18:13:25 2010 +0200
@@ -135,9 +135,9 @@
(* rhs *)
- val (_, tmp_lthy) = lthy |> Typedecl.predeclare_constraints (tname, raw_args, mx);
- val set = prep_term tmp_lthy raw_set;
- val tmp_lthy' = tmp_lthy |> Variable.declare_constraints set;
+ val tmp_ctxt = lthy |> fold (Variable.declare_typ o TFree) raw_args;
+ val set = prep_term tmp_ctxt raw_set;
+ val tmp_ctxt' = tmp_ctxt |> Variable.declare_term set;
val setT = Term.fastype_of set;
val oldT = HOLogic.dest_setT setT handle TYPE _ =>
@@ -149,7 +149,7 @@
(* lhs *)
- val args = map (fn (a, _) => (a, ProofContext.default_sort tmp_lthy' (a, ~1))) raw_args;
+ val args = map (ProofContext.check_tfree tmp_ctxt') raw_args;
val (newT, typedecl_lthy) = lthy
|> Typedecl.typedecl (tname, args, mx)
||> Variable.declare_term set;
--- a/src/HOLCF/Tools/pcpodef.ML Thu Apr 15 16:55:12 2010 +0200
+++ b/src/HOLCF/Tools/pcpodef.ML Thu Apr 15 18:13:25 2010 +0200
@@ -169,18 +169,18 @@
val _ = Theory.requires thy "Pcpodef" "pcpodefs";
(*rhs*)
- val (_, tmp_lthy) =
- thy |> Theory.copy |> Theory_Target.init NONE
- |> Typedecl.predeclare_constraints (tname, raw_args, mx);
- val set = prep_term tmp_lthy raw_set;
- val tmp_lthy' = tmp_lthy |> Variable.declare_constraints set;
+ val tmp_ctxt =
+ ProofContext.init thy
+ |> fold (Variable.declare_typ o TFree) raw_args;
+ val set = prep_term tmp_ctxt raw_set;
+ val tmp_ctxt' = tmp_ctxt |> Variable.declare_term set;
val setT = Term.fastype_of set;
val oldT = HOLogic.dest_setT setT handle TYPE _ =>
- error ("Not a set type: " ^ quote (Syntax.string_of_typ tmp_lthy setT));
+ error ("Not a set type: " ^ quote (Syntax.string_of_typ tmp_ctxt setT));
(*lhs*)
- val lhs_tfrees = map (fn (a, _) => (a, ProofContext.default_sort tmp_lthy' (a, ~1))) raw_args;
+ val lhs_tfrees = map (ProofContext.check_tfree tmp_ctxt') raw_args;
val full_tname = Sign.full_name thy tname;
val newT = Type (full_tname, map TFree lhs_tfrees);
--- a/src/HOLCF/Tools/repdef.ML Thu Apr 15 16:55:12 2010 +0200
+++ b/src/HOLCF/Tools/repdef.ML Thu Apr 15 18:13:25 2010 +0200
@@ -64,18 +64,18 @@
val _ = Theory.requires thy "Representable" "repdefs";
(*rhs*)
- val (_, tmp_lthy) =
- thy |> Theory.copy |> Theory_Target.init NONE
- |> Typedecl.predeclare_constraints (tname, raw_args, mx);
- val defl = prep_term tmp_lthy raw_defl;
- val tmp_lthy = tmp_lthy |> Variable.declare_constraints defl;
+ val tmp_ctxt =
+ ProofContext.init thy
+ |> fold (Variable.declare_typ o TFree) raw_args;
+ val defl = prep_term tmp_ctxt raw_defl;
+ val tmp_ctxt = tmp_ctxt |> Variable.declare_constraints defl;
val deflT = Term.fastype_of defl;
val _ = if deflT = @{typ "udom alg_defl"} then ()
- else error ("Not type udom alg_defl: " ^ quote (Syntax.string_of_typ tmp_lthy deflT));
+ else error ("Not type udom alg_defl: " ^ quote (Syntax.string_of_typ tmp_ctxt deflT));
(*lhs*)
- val lhs_tfrees = map (fn (a, _) => (a, ProofContext.default_sort tmp_lthy (a, ~1))) raw_args;
+ val lhs_tfrees = map (ProofContext.check_tfree tmp_ctxt) raw_args;
val lhs_sorts = map snd lhs_tfrees;
val full_tname = Sign.full_name thy tname;
val newT = Type (full_tname, map TFree lhs_tfrees);
--- a/src/Pure/Isar/proof_context.ML Thu Apr 15 16:55:12 2010 +0200
+++ b/src/Pure/Isar/proof_context.ML Thu Apr 15 18:13:25 2010 +0200
@@ -62,6 +62,8 @@
val read_const_proper: Proof.context -> bool -> string -> term
val read_const: Proof.context -> bool -> string -> term
val allow_dummies: Proof.context -> Proof.context
+ val check_tvar: Proof.context -> indexname * sort -> indexname * sort
+ val check_tfree: Proof.context -> string * sort -> string * sort
val decode_term: Proof.context -> term -> term
val standard_infer_types: Proof.context -> term list -> term list
val read_term_pattern: Proof.context -> string -> term
@@ -606,19 +608,26 @@
(* types *)
-fun get_sort ctxt def_sort raw_env =
+fun get_sort ctxt raw_env =
let
val tsig = tsig_of ctxt;
fun eq ((xi, S), (xi', S')) =
Term.eq_ix (xi, xi') andalso Type.eq_sort tsig (S, S');
val env = distinct eq raw_env;
- val _ = (case duplicates (eq_fst (op =)) env of [] => ()
+ val _ =
+ (case duplicates (eq_fst (op =)) env of
+ [] => ()
| dups => error ("Inconsistent sort constraints for type variable(s) "
^ commas_quote (map (Term.string_of_vname' o fst) dups)));
+ fun lookup xi =
+ (case AList.lookup (op =) env xi of
+ NONE => NONE
+ | SOME S => if S = dummyS then NONE else SOME S);
+
fun get xi =
- (case (AList.lookup (op =) env xi, def_sort xi) of
+ (case (lookup xi, Variable.def_sort ctxt xi) of
(NONE, NONE) => Type.defaultS tsig
| (NONE, SOME S) => S
| (SOME S, NONE) => S
@@ -629,6 +638,9 @@
" for type variable " ^ quote (Term.string_of_vname' xi)));
in get end;
+fun check_tvar ctxt (xi, S) = (xi, get_sort ctxt [(xi, S)] xi);
+fun check_tfree ctxt (x, S) = apfst fst (check_tvar ctxt ((x, ~1), S));
+
local
fun intern_skolem ctxt def_type x =
@@ -647,7 +659,7 @@
in
fun term_context ctxt =
- {get_sort = get_sort ctxt (Variable.def_sort ctxt),
+ {get_sort = get_sort ctxt,
map_const = fn a => ((true, #1 (Term.dest_Const (read_const_proper ctxt false a)))
handle ERROR _ => (false, Consts.intern (consts_of ctxt) a)),
map_free = intern_skolem ctxt (Variable.def_type ctxt false)};
@@ -731,9 +743,8 @@
fun parse_typ ctxt text =
let
- val get_sort = get_sort ctxt (Variable.def_sort ctxt);
val (syms, pos) = Syntax.parse_token Markup.typ text;
- val T = Syntax.standard_parse_typ ctxt (syn_of ctxt) get_sort (syms, pos)
+ val T = Syntax.standard_parse_typ ctxt (syn_of ctxt) (get_sort ctxt) (syms, pos)
handle ERROR msg => cat_error msg ("Failed to parse type" ^ Position.str_of pos);
in T end;
--- a/src/Pure/Isar/typedecl.ML Thu Apr 15 16:55:12 2010 +0200
+++ b/src/Pure/Isar/typedecl.ML Thu Apr 15 18:13:25 2010 +0200
@@ -7,8 +7,7 @@
signature TYPEDECL =
sig
val read_constraint: Proof.context -> string option -> sort
- val predeclare_constraints: binding * (string * sort) list * mixfix ->
- local_theory -> string * local_theory
+ val basic_typedecl: binding * int * mixfix -> local_theory -> string * local_theory
val typedecl: binding * (string * sort) list * mixfix -> local_theory -> typ * local_theory
val typedecl_global: binding * (string * sort) list * mixfix -> theory -> typ * theory
end;
@@ -16,6 +15,12 @@
structure Typedecl: TYPEDECL =
struct
+(* constraints *)
+
+fun read_constraint _ NONE = dummyS
+ | read_constraint ctxt (SOME s) = Syntax.read_sort ctxt s;
+
+
(* primitives *)
fun object_logic_arity name thy =
@@ -33,17 +38,7 @@
end;
-(* syntactic version -- useful for internalizing additional types/terms beforehand *)
-
-fun read_constraint _ NONE = dummyS
- | read_constraint ctxt (SOME s) = Syntax.read_sort ctxt s;
-
-fun predeclare_constraints (b, raw_args, mx) =
- basic_typedecl (b, length raw_args, mx) ##>
- fold (Variable.declare_constraints o Logic.mk_type o TFree) raw_args;
-
-
-(* regular version -- without dependencies on type parameters of the context *)
+(* regular typedecl -- without dependencies on type parameters of the context *)
fun typedecl (b, raw_args, mx) lthy =
let
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML Thu Apr 15 16:55:12 2010 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Thu Apr 15 18:13:25 2010 +0200
@@ -955,7 +955,7 @@
end)
| _ => raise PGIP "Invalid PGIP packet received")
handle PGIP msg =>
- (Output.error_msg ((msg ^ "\nPGIP error occured in XML text below:\n") ^
+ (Output.error_msg ((msg ^ "\nPGIP error occurred in XML text below:\n") ^
(XML.string_of xml));
true))