dropped some unused bindings
authorhaftmann
Mon Nov 30 12:28:12 2009 +0100 (2009-11-30 ago)
changeset 339691e7ca47c6c3d
parent 33968 f94fb13ecbb3
child 33970 74db95c74f89
dropped some unused bindings
src/HOL/Tools/Datatype/datatype.ML
src/HOL/Tools/Datatype/datatype_case.ML
src/HOL/Tools/Datatype/datatype_data.ML
src/HOL/Tools/Datatype/datatype_realizer.ML
src/Pure/Isar/class_target.ML
src/Pure/Isar/code.ML
src/Pure/axclass.ML
src/Tools/Code/code_haskell.ML
src/Tools/Code/code_target.ML
src/Tools/Code/code_thingol.ML
     1.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Mon Nov 30 11:42:49 2009 +0100
     1.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Mon Nov 30 12:28:12 2009 +0100
     1.3 @@ -36,7 +36,6 @@
     1.4  val In1_name = @{const_name "Datatype.In1"};
     1.5  val Scons_name = @{const_name "Datatype.Scons"};
     1.6  val Leaf_name = @{const_name "Datatype.Leaf"};
     1.7 -val Numb_name = @{const_name "Datatype.Numb"};
     1.8  val Lim_name = @{const_name "Datatype.Lim"};
     1.9  val Suml_name = @{const_name "Sum_Type.Suml"};
    1.10  val Sumr_name = @{const_name "Sum_Type.Sumr"};
     2.1 --- a/src/HOL/Tools/Datatype/datatype_case.ML	Mon Nov 30 11:42:49 2009 +0100
     2.2 +++ b/src/HOL/Tools/Datatype/datatype_case.ML	Mon Nov 30 12:28:12 2009 +0100
     2.3 @@ -227,7 +227,6 @@
     2.4                    val nrows = maps (expand constructors used' pty) rows;
     2.5                    val subproblems = partition ty_match ty_inst type_of used'
     2.6                      constructors pty range_ty nrows;
     2.7 -                  val new_formals = map #new_formals subproblems
     2.8                    val constructors' = map #constructor subproblems
     2.9                    val news = map (fn {new_formals, group, ...} =>
    2.10                      {path = new_formals @ rstp, rows = group}) subproblems;
     3.1 --- a/src/HOL/Tools/Datatype/datatype_data.ML	Mon Nov 30 11:42:49 2009 +0100
     3.2 +++ b/src/HOL/Tools/Datatype/datatype_data.ML	Mon Nov 30 12:28:12 2009 +0100
     3.3 @@ -101,7 +101,7 @@
     3.4  
     3.5  fun the_spec thy dtco =
     3.6    let
     3.7 -    val info as { descr, index, sorts = raw_sorts, ... } = the_info thy dtco;
     3.8 +    val { descr, index, sorts = raw_sorts, ... } = the_info thy dtco;
     3.9      val SOME (_, dtys, raw_cos) = AList.lookup (op =) descr index;
    3.10      val sorts = map ((fn v => (v, (the o AList.lookup (op =) raw_sorts) v))
    3.11        o Datatype_Aux.dest_DtTFree) dtys;
    3.12 @@ -114,7 +114,7 @@
    3.13      val info = the_info thy raw_tyco;
    3.14      val descr = #descr info;
    3.15  
    3.16 -    val SOME (_, dtys, raw_cos) = AList.lookup (op =) descr (#index info);
    3.17 +    val SOME (_, dtys, _) = AList.lookup (op =) descr (#index info);
    3.18      val vs = map ((fn v => (v, (the o AList.lookup (op =) (#sorts info)) v))
    3.19        o dest_DtTFree) dtys;
    3.20  
     4.1 --- a/src/HOL/Tools/Datatype/datatype_realizer.ML	Mon Nov 30 11:42:49 2009 +0100
     4.2 +++ b/src/HOL/Tools/Datatype/datatype_realizer.ML	Mon Nov 30 12:28:12 2009 +0100
     4.3 @@ -28,16 +28,11 @@
     4.4  fun prf_of thm =
     4.5    Reconstruct.reconstruct_proof (Thm.theory_of_thm thm) (Thm.prop_of thm) (Thm.proof_of thm);
     4.6  
     4.7 -fun prf_subst_vars inst =
     4.8 -  Proofterm.map_proof_terms (subst_vars ([], inst)) I;
     4.9 -
    4.10  fun is_unit t = snd (strip_type (fastype_of t)) = HOLogic.unitT;
    4.11  
    4.12  fun tname_of (Type (s, _)) = s
    4.13    | tname_of _ = "";
    4.14  
    4.15 -fun mk_realizes T = Const ("realizes", T --> HOLogic.boolT --> HOLogic.boolT);
    4.16 -
    4.17  fun make_ind sorts ({descr, rec_names, rec_rewrites, induct, ...} : info) is thy =
    4.18    let
    4.19      val recTs = get_rec_types descr sorts;
     5.1 --- a/src/Pure/Isar/class_target.ML	Mon Nov 30 11:42:49 2009 +0100
     5.2 +++ b/src/Pure/Isar/class_target.ML	Mon Nov 30 12:28:12 2009 +0100
     5.3 @@ -278,7 +278,7 @@
     5.4      fun improve (c, ty) = (case AList.lookup (op =) primary_constraints c
     5.5       of SOME ty' => (case try (Type.raw_match (ty', ty)) Vartab.empty
     5.6           of SOME tyenv => (case Vartab.lookup tyenv (Name.aT, 0)
     5.7 -             of SOME (_, ty' as TVar (tvar as (vi, sort))) =>
     5.8 +             of SOME (_, ty' as TVar (vi, sort)) =>
     5.9                    if TypeInfer.is_param vi
    5.10                      andalso Sorts.sort_le algebra (base_sort, sort)
    5.11                        then SOME (ty', TFree (Name.aT, base_sort))
    5.12 @@ -434,9 +434,10 @@
    5.13  
    5.14  fun synchronize_inst_syntax ctxt =
    5.15    let
    5.16 -    val Instantiation { arities = (_, _, sort), params = params } = Instantiation.get ctxt;
    5.17 +    val Instantiation { params, ... } = Instantiation.get ctxt;
    5.18  
    5.19 -    val lookup_inst_param = AxClass.lookup_inst_param (Sign.consts_of (ProofContext.theory_of ctxt)) params;
    5.20 +    val lookup_inst_param = AxClass.lookup_inst_param
    5.21 +      (Sign.consts_of (ProofContext.theory_of ctxt)) params;
    5.22      fun subst (c, ty) = case lookup_inst_param (c, ty)
    5.23       of SOME (v_ty as (_, ty)) => SOME (ty, Free v_ty)
    5.24        | NONE => NONE;
    5.25 @@ -563,8 +564,7 @@
    5.26  
    5.27  fun conclude_instantiation lthy =
    5.28    let
    5.29 -    val { arities, params } = the_instantiation lthy;
    5.30 -    val (tycos, vs, sort) = arities;
    5.31 +    val (tycos, vs, sort) = (#arities o the_instantiation) lthy;
    5.32      val thy = ProofContext.theory_of lthy;
    5.33      val _ = map (fn tyco => if Sign.of_sort thy
    5.34          (Type (tyco, map TFree vs), sort)
    5.35 @@ -574,8 +574,7 @@
    5.36  
    5.37  fun pretty_instantiation lthy =
    5.38    let
    5.39 -    val { arities, params } = the_instantiation lthy;
    5.40 -    val (tycos, vs, sort) = arities;
    5.41 +    val { arities = (tycos, vs, sort), params } = the_instantiation lthy;
    5.42      val thy = ProofContext.theory_of lthy;
    5.43      fun pr_arity tyco = Syntax.pretty_arity lthy (tyco, map snd vs, sort);
    5.44      fun pr_param ((c, _), (v, ty)) =
     6.1 --- a/src/Pure/Isar/code.ML	Mon Nov 30 11:42:49 2009 +0100
     6.2 +++ b/src/Pure/Isar/code.ML	Mon Nov 30 12:28:12 2009 +0100
     6.3 @@ -240,7 +240,7 @@
     6.4      (Symtab.empty, (Symtab.empty, (Symtab.empty, Symtab.empty)))), Unsynchronized.ref empty_data);
     6.5    fun copy (spec, data) = (spec, Unsynchronized.ref (! data));
     6.6    val extend = copy;
     6.7 -  fun merge pp ((spec1, data1), (spec2, data2)) =
     6.8 +  fun merge _ ((spec1, _), (spec2, _)) =
     6.9      (merge_spec (spec1, spec2), Unsynchronized.ref empty_data);
    6.10  );
    6.11  
    6.12 @@ -511,7 +511,7 @@
    6.13                |> map (fn v => TFree (v, []));
    6.14          val ty = typ_subst_TVars (tvars ~~ tvars') raw_ty;
    6.15        in typscheme thy (c, ty) end
    6.16 -  | typscheme_eqns thy c (thms as thm :: _) = typscheme_eqn thy thm;
    6.17 +  | typscheme_eqns thy c (thm :: _) = typscheme_eqn thy thm;
    6.18  
    6.19  fun assert_eqns_const thy c eqns =
    6.20    let
     7.1 --- a/src/Pure/axclass.ML	Mon Nov 30 11:42:49 2009 +0100
     7.2 +++ b/src/Pure/axclass.ML	Mon Nov 30 12:28:12 2009 +0100
     7.3 @@ -257,12 +257,11 @@
     7.4    | NONE => NONE;
     7.5  
     7.6  fun unoverload_const thy (c_ty as (c, _)) =
     7.7 -  case class_of_param thy c
     7.8 -   of SOME class (* FIXME unused? *) =>
     7.9 -     (case get_inst_tyco (Sign.consts_of thy) c_ty
    7.10 -       of SOME tyco => try (param_of_inst thy) (c, tyco) |> the_default c
    7.11 -        | NONE => c)
    7.12 -    | NONE => c;
    7.13 +  if is_some (class_of_param thy c)
    7.14 +  then case get_inst_tyco (Sign.consts_of thy) c_ty
    7.15 +   of SOME tyco => try (param_of_inst thy) (c, tyco) |> the_default c
    7.16 +    | NONE => c
    7.17 +  else c;
    7.18  
    7.19  
    7.20  (** instances **)
     8.1 --- a/src/Tools/Code/code_haskell.ML	Mon Nov 30 11:42:49 2009 +0100
     8.2 +++ b/src/Tools/Code/code_haskell.ML	Mon Nov 30 12:28:12 2009 +0100
     8.3 @@ -42,7 +42,7 @@
     8.4            (map (str o lookup_var tyvars) vnames) @ str "." @@ Pretty.brk 1;
     8.5      fun pr_tycoexpr tyvars fxy (tyco, tys) =
     8.6        brackify fxy (str tyco :: map (pr_typ tyvars BR) tys)
     8.7 -    and pr_typ tyvars fxy (tycoexpr as tyco `%% tys) = (case syntax_tyco tyco
     8.8 +    and pr_typ tyvars fxy (tyco `%% tys) = (case syntax_tyco tyco
     8.9           of NONE => pr_tycoexpr tyvars fxy (deresolve tyco, tys)
    8.10            | SOME (i, pr) => pr (pr_typ tyvars) fxy tys)
    8.11        | pr_typ tyvars fxy (ITyVar v) = (str o lookup_var tyvars) v;
     9.1 --- a/src/Tools/Code/code_target.ML	Mon Nov 30 11:42:49 2009 +0100
     9.2 +++ b/src/Tools/Code/code_target.ML	Mon Nov 30 12:28:12 2009 +0100
     9.3 @@ -46,6 +46,7 @@
     9.4    val add_syntax_tyco: string -> string -> tyco_syntax option -> theory -> theory
     9.5    val add_syntax_const: string -> string -> proto_const_syntax option -> theory -> theory
     9.6    val add_reserved: string -> string -> theory -> theory
     9.7 +  val add_include: string -> string * (string * string list) option -> theory -> theory
     9.8  end;
     9.9  
    9.10  structure Code_Target : CODE_TARGET =
    9.11 @@ -165,10 +166,9 @@
    9.12  
    9.13  val abort_allowed = snd o CodeTargetData.get;
    9.14  
    9.15 -fun assert_target thy target =
    9.16 -  case Symtab.lookup (fst (CodeTargetData.get thy)) target
    9.17 -   of SOME data => target
    9.18 -    | NONE => error ("Unknown code target language: " ^ quote target);
    9.19 +fun assert_target thy target = if Symtab.defined (fst (CodeTargetData.get thy)) target
    9.20 +  then target
    9.21 +  else error ("Unknown code target language: " ^ quote target);
    9.22  
    9.23  fun put_target (target, seri) thy =
    9.24    let
    9.25 @@ -238,7 +238,7 @@
    9.26  
    9.27  fun read_tyco thy = cert_tyco thy o Sign.intern_type thy;
    9.28  
    9.29 -fun gen_add_syntax_class prep_class prep_const target raw_class raw_syn thy =
    9.30 +fun gen_add_syntax_class prep_class target raw_class raw_syn thy =
    9.31    let
    9.32      val class = prep_class thy raw_class;
    9.33    in case raw_syn
    9.34 @@ -318,7 +318,7 @@
    9.35        | add (name, NONE) incls = Symtab.delete name incls;
    9.36    in map_includes target (add args) thy end;
    9.37  
    9.38 -val add_include = gen_add_include Code.check_const;
    9.39 +val add_include = gen_add_include (K I);
    9.40  val add_include_cmd = gen_add_include Code.read_const;
    9.41  
    9.42  fun add_module_alias target (thyname, modlname) =
    9.43 @@ -355,14 +355,15 @@
    9.44  
    9.45  in
    9.46  
    9.47 -val add_syntax_class = gen_add_syntax_class cert_class (K I);
    9.48 +val add_syntax_class = gen_add_syntax_class cert_class;
    9.49  val add_syntax_inst = gen_add_syntax_inst cert_class cert_tyco;
    9.50  val add_syntax_tyco = gen_add_syntax_tyco cert_tyco;
    9.51  val add_syntax_const = gen_add_syntax_const (K I);
    9.52  val allow_abort = gen_allow_abort (K I);
    9.53  val add_reserved = add_reserved;
    9.54 +val add_include = add_include;
    9.55  
    9.56 -val add_syntax_class_cmd = gen_add_syntax_class read_class Code.read_const;
    9.57 +val add_syntax_class_cmd = gen_add_syntax_class read_class;
    9.58  val add_syntax_inst_cmd = gen_add_syntax_inst read_class read_tyco;
    9.59  val add_syntax_tyco_cmd = gen_add_syntax_tyco read_tyco;
    9.60  val add_syntax_const_cmd = gen_add_syntax_const Code.read_const;
    9.61 @@ -606,7 +607,7 @@
    9.62      ((filter OuterLex.is_proper o OuterSyntax.scan Position.none) cmd)
    9.63     of SOME f => (writeln "Now generating code..."; f (theory thyname))
    9.64      | NONE => error ("Bad directive " ^ quote cmd)))
    9.65 -  handle TOPLEVEL_ERROR => OS.Process.exit OS.Process.failure;
    9.66 +  handle Runtime.TOPLEVEL_ERROR => OS.Process.exit OS.Process.failure;
    9.67  
    9.68  end; (*local*)
    9.69  
    10.1 --- a/src/Tools/Code/code_thingol.ML	Mon Nov 30 11:42:49 2009 +0100
    10.2 +++ b/src/Tools/Code/code_thingol.ML	Mon Nov 30 12:28:12 2009 +0100
    10.3 @@ -930,10 +930,7 @@
    10.4            ((snd o #constants o Consts.dest o #consts o Sign.rep_sg) thy') [];
    10.5          fun belongs_here c =
    10.6            not (exists (fn thy'' => Sign.declared_const thy'' c) (Theory.parents_of thy'))
    10.7 -      in case some_thyname
    10.8 -       of NONE => cs
    10.9 -        | SOME thyname => filter belongs_here cs
   10.10 -      end;
   10.11 +      in if is_some some_thyname then cs else filter belongs_here cs end;
   10.12      fun read_const_expr "*" = ([], consts_of NONE)
   10.13        | read_const_expr s = if String.isSuffix ".*" s
   10.14            then ([], consts_of (SOME (unsuffix ".*" s)))