--- a/src/HOL/Tools/Datatype/datatype.ML Mon Nov 30 11:42:49 2009 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML Mon Nov 30 12:28:12 2009 +0100
@@ -36,7 +36,6 @@
val In1_name = @{const_name "Datatype.In1"};
val Scons_name = @{const_name "Datatype.Scons"};
val Leaf_name = @{const_name "Datatype.Leaf"};
-val Numb_name = @{const_name "Datatype.Numb"};
val Lim_name = @{const_name "Datatype.Lim"};
val Suml_name = @{const_name "Sum_Type.Suml"};
val Sumr_name = @{const_name "Sum_Type.Sumr"};
--- a/src/HOL/Tools/Datatype/datatype_case.ML Mon Nov 30 11:42:49 2009 +0100
+++ b/src/HOL/Tools/Datatype/datatype_case.ML Mon Nov 30 12:28:12 2009 +0100
@@ -227,7 +227,6 @@
val nrows = maps (expand constructors used' pty) rows;
val subproblems = partition ty_match ty_inst type_of used'
constructors pty range_ty nrows;
- val new_formals = map #new_formals subproblems
val constructors' = map #constructor subproblems
val news = map (fn {new_formals, group, ...} =>
{path = new_formals @ rstp, rows = group}) subproblems;
--- a/src/HOL/Tools/Datatype/datatype_data.ML Mon Nov 30 11:42:49 2009 +0100
+++ b/src/HOL/Tools/Datatype/datatype_data.ML Mon Nov 30 12:28:12 2009 +0100
@@ -101,7 +101,7 @@
fun the_spec thy dtco =
let
- val info as { descr, index, sorts = raw_sorts, ... } = the_info thy dtco;
+ val { descr, index, sorts = raw_sorts, ... } = the_info thy dtco;
val SOME (_, dtys, raw_cos) = AList.lookup (op =) descr index;
val sorts = map ((fn v => (v, (the o AList.lookup (op =) raw_sorts) v))
o Datatype_Aux.dest_DtTFree) dtys;
@@ -114,7 +114,7 @@
val info = the_info thy raw_tyco;
val descr = #descr info;
- val SOME (_, dtys, raw_cos) = AList.lookup (op =) descr (#index info);
+ val SOME (_, dtys, _) = AList.lookup (op =) descr (#index info);
val vs = map ((fn v => (v, (the o AList.lookup (op =) (#sorts info)) v))
o dest_DtTFree) dtys;
--- a/src/HOL/Tools/Datatype/datatype_realizer.ML Mon Nov 30 11:42:49 2009 +0100
+++ b/src/HOL/Tools/Datatype/datatype_realizer.ML Mon Nov 30 12:28:12 2009 +0100
@@ -28,16 +28,11 @@
fun prf_of thm =
Reconstruct.reconstruct_proof (Thm.theory_of_thm thm) (Thm.prop_of thm) (Thm.proof_of thm);
-fun prf_subst_vars inst =
- Proofterm.map_proof_terms (subst_vars ([], inst)) I;
-
fun is_unit t = snd (strip_type (fastype_of t)) = HOLogic.unitT;
fun tname_of (Type (s, _)) = s
| tname_of _ = "";
-fun mk_realizes T = Const ("realizes", T --> HOLogic.boolT --> HOLogic.boolT);
-
fun make_ind sorts ({descr, rec_names, rec_rewrites, induct, ...} : info) is thy =
let
val recTs = get_rec_types descr sorts;
--- a/src/Pure/Isar/class_target.ML Mon Nov 30 11:42:49 2009 +0100
+++ b/src/Pure/Isar/class_target.ML Mon Nov 30 12:28:12 2009 +0100
@@ -278,7 +278,7 @@
fun improve (c, ty) = (case AList.lookup (op =) primary_constraints c
of SOME ty' => (case try (Type.raw_match (ty', ty)) Vartab.empty
of SOME tyenv => (case Vartab.lookup tyenv (Name.aT, 0)
- of SOME (_, ty' as TVar (tvar as (vi, sort))) =>
+ of SOME (_, ty' as TVar (vi, sort)) =>
if TypeInfer.is_param vi
andalso Sorts.sort_le algebra (base_sort, sort)
then SOME (ty', TFree (Name.aT, base_sort))
@@ -434,9 +434,10 @@
fun synchronize_inst_syntax ctxt =
let
- val Instantiation { arities = (_, _, sort), params = params } = Instantiation.get ctxt;
+ val Instantiation { params, ... } = Instantiation.get ctxt;
- val lookup_inst_param = AxClass.lookup_inst_param (Sign.consts_of (ProofContext.theory_of ctxt)) params;
+ val lookup_inst_param = AxClass.lookup_inst_param
+ (Sign.consts_of (ProofContext.theory_of ctxt)) params;
fun subst (c, ty) = case lookup_inst_param (c, ty)
of SOME (v_ty as (_, ty)) => SOME (ty, Free v_ty)
| NONE => NONE;
@@ -563,8 +564,7 @@
fun conclude_instantiation lthy =
let
- val { arities, params } = the_instantiation lthy;
- val (tycos, vs, sort) = arities;
+ val (tycos, vs, sort) = (#arities o the_instantiation) lthy;
val thy = ProofContext.theory_of lthy;
val _ = map (fn tyco => if Sign.of_sort thy
(Type (tyco, map TFree vs), sort)
@@ -574,8 +574,7 @@
fun pretty_instantiation lthy =
let
- val { arities, params } = the_instantiation lthy;
- val (tycos, vs, sort) = arities;
+ val { arities = (tycos, vs, sort), params } = the_instantiation lthy;
val thy = ProofContext.theory_of lthy;
fun pr_arity tyco = Syntax.pretty_arity lthy (tyco, map snd vs, sort);
fun pr_param ((c, _), (v, ty)) =
--- a/src/Pure/Isar/code.ML Mon Nov 30 11:42:49 2009 +0100
+++ b/src/Pure/Isar/code.ML Mon Nov 30 12:28:12 2009 +0100
@@ -240,7 +240,7 @@
(Symtab.empty, (Symtab.empty, (Symtab.empty, Symtab.empty)))), Unsynchronized.ref empty_data);
fun copy (spec, data) = (spec, Unsynchronized.ref (! data));
val extend = copy;
- fun merge pp ((spec1, data1), (spec2, data2)) =
+ fun merge _ ((spec1, _), (spec2, _)) =
(merge_spec (spec1, spec2), Unsynchronized.ref empty_data);
);
@@ -511,7 +511,7 @@
|> map (fn v => TFree (v, []));
val ty = typ_subst_TVars (tvars ~~ tvars') raw_ty;
in typscheme thy (c, ty) end
- | typscheme_eqns thy c (thms as thm :: _) = typscheme_eqn thy thm;
+ | typscheme_eqns thy c (thm :: _) = typscheme_eqn thy thm;
fun assert_eqns_const thy c eqns =
let
--- a/src/Pure/axclass.ML Mon Nov 30 11:42:49 2009 +0100
+++ b/src/Pure/axclass.ML Mon Nov 30 12:28:12 2009 +0100
@@ -257,12 +257,11 @@
| NONE => NONE;
fun unoverload_const thy (c_ty as (c, _)) =
- case class_of_param thy c
- of SOME class (* FIXME unused? *) =>
- (case get_inst_tyco (Sign.consts_of thy) c_ty
- of SOME tyco => try (param_of_inst thy) (c, tyco) |> the_default c
- | NONE => c)
- | NONE => c;
+ if is_some (class_of_param thy c)
+ then case get_inst_tyco (Sign.consts_of thy) c_ty
+ of SOME tyco => try (param_of_inst thy) (c, tyco) |> the_default c
+ | NONE => c
+ else c;
(** instances **)
--- a/src/Tools/Code/code_haskell.ML Mon Nov 30 11:42:49 2009 +0100
+++ b/src/Tools/Code/code_haskell.ML Mon Nov 30 12:28:12 2009 +0100
@@ -42,7 +42,7 @@
(map (str o lookup_var tyvars) vnames) @ str "." @@ Pretty.brk 1;
fun pr_tycoexpr tyvars fxy (tyco, tys) =
brackify fxy (str tyco :: map (pr_typ tyvars BR) tys)
- and pr_typ tyvars fxy (tycoexpr as tyco `%% tys) = (case syntax_tyco tyco
+ and pr_typ tyvars fxy (tyco `%% tys) = (case syntax_tyco tyco
of NONE => pr_tycoexpr tyvars fxy (deresolve tyco, tys)
| SOME (i, pr) => pr (pr_typ tyvars) fxy tys)
| pr_typ tyvars fxy (ITyVar v) = (str o lookup_var tyvars) v;
--- a/src/Tools/Code/code_target.ML Mon Nov 30 11:42:49 2009 +0100
+++ b/src/Tools/Code/code_target.ML Mon Nov 30 12:28:12 2009 +0100
@@ -46,6 +46,7 @@
val add_syntax_tyco: string -> string -> tyco_syntax option -> theory -> theory
val add_syntax_const: string -> string -> proto_const_syntax option -> theory -> theory
val add_reserved: string -> string -> theory -> theory
+ val add_include: string -> string * (string * string list) option -> theory -> theory
end;
structure Code_Target : CODE_TARGET =
@@ -165,10 +166,9 @@
val abort_allowed = snd o CodeTargetData.get;
-fun assert_target thy target =
- case Symtab.lookup (fst (CodeTargetData.get thy)) target
- of SOME data => target
- | NONE => error ("Unknown code target language: " ^ quote target);
+fun assert_target thy target = if Symtab.defined (fst (CodeTargetData.get thy)) target
+ then target
+ else error ("Unknown code target language: " ^ quote target);
fun put_target (target, seri) thy =
let
@@ -238,7 +238,7 @@
fun read_tyco thy = cert_tyco thy o Sign.intern_type thy;
-fun gen_add_syntax_class prep_class prep_const target raw_class raw_syn thy =
+fun gen_add_syntax_class prep_class target raw_class raw_syn thy =
let
val class = prep_class thy raw_class;
in case raw_syn
@@ -318,7 +318,7 @@
| add (name, NONE) incls = Symtab.delete name incls;
in map_includes target (add args) thy end;
-val add_include = gen_add_include Code.check_const;
+val add_include = gen_add_include (K I);
val add_include_cmd = gen_add_include Code.read_const;
fun add_module_alias target (thyname, modlname) =
@@ -355,14 +355,15 @@
in
-val add_syntax_class = gen_add_syntax_class cert_class (K I);
+val add_syntax_class = gen_add_syntax_class cert_class;
val add_syntax_inst = gen_add_syntax_inst cert_class cert_tyco;
val add_syntax_tyco = gen_add_syntax_tyco cert_tyco;
val add_syntax_const = gen_add_syntax_const (K I);
val allow_abort = gen_allow_abort (K I);
val add_reserved = add_reserved;
+val add_include = add_include;
-val add_syntax_class_cmd = gen_add_syntax_class read_class Code.read_const;
+val add_syntax_class_cmd = gen_add_syntax_class read_class;
val add_syntax_inst_cmd = gen_add_syntax_inst read_class read_tyco;
val add_syntax_tyco_cmd = gen_add_syntax_tyco read_tyco;
val add_syntax_const_cmd = gen_add_syntax_const Code.read_const;
@@ -606,7 +607,7 @@
((filter OuterLex.is_proper o OuterSyntax.scan Position.none) cmd)
of SOME f => (writeln "Now generating code..."; f (theory thyname))
| NONE => error ("Bad directive " ^ quote cmd)))
- handle TOPLEVEL_ERROR => OS.Process.exit OS.Process.failure;
+ handle Runtime.TOPLEVEL_ERROR => OS.Process.exit OS.Process.failure;
end; (*local*)
--- a/src/Tools/Code/code_thingol.ML Mon Nov 30 11:42:49 2009 +0100
+++ b/src/Tools/Code/code_thingol.ML Mon Nov 30 12:28:12 2009 +0100
@@ -930,10 +930,7 @@
((snd o #constants o Consts.dest o #consts o Sign.rep_sg) thy') [];
fun belongs_here c =
not (exists (fn thy'' => Sign.declared_const thy'' c) (Theory.parents_of thy'))
- in case some_thyname
- of NONE => cs
- | SOME thyname => filter belongs_here cs
- end;
+ in if is_some some_thyname then cs else filter belongs_here cs end;
fun read_const_expr "*" = ([], consts_of NONE)
| read_const_expr s = if String.isSuffix ".*" s
then ([], consts_of (SOME (unsuffix ".*" s)))