# HG changeset patch # User haftmann # Date 1259580492 -3600 # Node ID 1e7ca47c6c3daaa8f867fd33d7058cea84990b24 # Parent f94fb13ecbb3739f6ad080bb3546422d6e5aeb0c dropped some unused bindings diff -r f94fb13ecbb3 -r 1e7ca47c6c3d src/HOL/Tools/Datatype/datatype.ML --- 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"}; diff -r f94fb13ecbb3 -r 1e7ca47c6c3d src/HOL/Tools/Datatype/datatype_case.ML --- 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; diff -r f94fb13ecbb3 -r 1e7ca47c6c3d src/HOL/Tools/Datatype/datatype_data.ML --- 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; diff -r f94fb13ecbb3 -r 1e7ca47c6c3d src/HOL/Tools/Datatype/datatype_realizer.ML --- 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; diff -r f94fb13ecbb3 -r 1e7ca47c6c3d src/Pure/Isar/class_target.ML --- 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)) = diff -r f94fb13ecbb3 -r 1e7ca47c6c3d src/Pure/Isar/code.ML --- 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 diff -r f94fb13ecbb3 -r 1e7ca47c6c3d src/Pure/axclass.ML --- 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 **) diff -r f94fb13ecbb3 -r 1e7ca47c6c3d src/Tools/Code/code_haskell.ML --- 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; diff -r f94fb13ecbb3 -r 1e7ca47c6c3d src/Tools/Code/code_target.ML --- 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*) diff -r f94fb13ecbb3 -r 1e7ca47c6c3d src/Tools/Code/code_thingol.ML --- 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)))