src/Pure/theory.ML
changeset 18943 947d3a694654
parent 18857 c4b4fbd74ffb
child 18968 52639ad19a96
     1.1 --- a/src/Pure/theory.ML	Mon Feb 06 20:59:09 2006 +0100
     1.2 +++ b/src/Pure/theory.ML	Mon Feb 06 20:59:10 2006 +0100
     1.3 @@ -45,7 +45,6 @@
     1.4    val merge_refs: theory_ref * theory_ref -> theory_ref    (*exception TERM*)
     1.5    val requires: theory -> string -> string -> unit
     1.6    val assert_super: theory -> theory -> theory
     1.7 -  val dest_def: Pretty.pp -> term -> (string * typ) * term
     1.8    val add_axioms: (bstring * string) list -> theory -> theory
     1.9    val add_axioms_i: (bstring * term) list -> theory -> theory
    1.10    val add_defs: bool -> (bstring * string) list -> theory -> theory
    1.11 @@ -166,13 +165,6 @@
    1.12  fun err_in_axm msg name =
    1.13    cat_error msg ("The error(s) above occurred in axiom " ^ quote name);
    1.14  
    1.15 -fun no_vars pp tm =
    1.16 -  (case (Term.term_vars tm, Term.term_tvars tm) of
    1.17 -    ([], []) => tm
    1.18 -  | (ts, ixns) => error (Pretty.string_of (Pretty.block (Pretty.breaks
    1.19 -      (Pretty.str "Illegal schematic variable(s) in term:" ::
    1.20 -       map (Pretty.term pp) ts @ map (Pretty.typ pp o TVar) ixns)))));
    1.21 -
    1.22  fun cert_axm thy (name, raw_tm) =
    1.23    let
    1.24      val pp = Sign.pp thy;
    1.25 @@ -182,7 +174,7 @@
    1.26    in
    1.27      Term.no_dummy_patterns t handle TERM (msg, _) => error msg;
    1.28      assert (T = propT) "Term not of type prop";
    1.29 -    (name, no_vars pp t)
    1.30 +    (name, Sign.no_vars pp t)
    1.31    end;
    1.32  
    1.33  fun read_def_axm (thy, types, sorts) used (name, str) =
    1.34 @@ -198,7 +190,7 @@
    1.35    let
    1.36      val pp = Sign.pp thy;
    1.37      val (t, _) = Sign.infer_types pp thy (K NONE) (K NONE) [] true ([pre_tm], propT);
    1.38 -  in (name, no_vars pp t) end
    1.39 +  in (name, Sign.no_vars pp t) end
    1.40    handle ERROR msg => err_in_axm msg name;
    1.41  
    1.42  
    1.43 @@ -252,45 +244,6 @@
    1.44    end;
    1.45  
    1.46  
    1.47 -(* dest_def *)
    1.48 -
    1.49 -fun dest_def pp tm =
    1.50 -  let
    1.51 -    fun err msg = raise TERM (msg, [tm]);
    1.52 -
    1.53 -    val (lhs, rhs) = Logic.dest_equals (Logic.strip_imp_concl tm)
    1.54 -      handle TERM _ => err "Not a meta-equality (==)";
    1.55 -    val (head, args) = Term.strip_comb (Pattern.beta_eta_contract lhs);
    1.56 -    val (c, T) = Term.dest_Const head
    1.57 -      handle TERM _ => err "Head of lhs not a constant";
    1.58 -
    1.59 -    fun dest_free (Free (x, _)) = x
    1.60 -      | dest_free (Const ("TYPE", Type ("itself", [TFree (x, _)]))) = x
    1.61 -      | dest_free _ = raise Match;
    1.62 -
    1.63 -    val show_terms = commas_quote o map (Pretty.string_of_term pp);
    1.64 -    val show_frees = commas_quote o map dest_free;
    1.65 -    val show_tfrees = commas_quote o map fst;
    1.66 -
    1.67 -    val lhs_nofrees = filter (not o can dest_free) args;
    1.68 -    val lhs_dups = gen_duplicates (op aconv) args;
    1.69 -    val rhs_extras = term_frees rhs |> fold (remove op aconv) args;
    1.70 -    val rhs_extrasT = term_tfrees rhs |> fold (remove op =) (typ_tfrees T);
    1.71 -  in
    1.72 -    if not (null lhs_nofrees) then
    1.73 -      err ("Non-variables as arguments on lhs: " ^ show_terms lhs_nofrees)
    1.74 -    else if not (null lhs_dups) then
    1.75 -      err ("Duplicate variables on lhs: " ^ show_frees lhs_dups)
    1.76 -    else if not (null rhs_extras) then
    1.77 -      err ("Extra variables on rhs: " ^ show_frees rhs_extras)
    1.78 -    else if not (null rhs_extrasT) then
    1.79 -      err ("Extra type variables on rhs: " ^ show_tfrees rhs_extrasT)
    1.80 -    else if exists_Const (equal (c, T)) rhs then
    1.81 -      err ("Constant to be defined occurs on rhs")
    1.82 -    else ((c, T), rhs)
    1.83 -  end;
    1.84 -
    1.85 -
    1.86  (* check_def *)
    1.87  
    1.88  fun check_def thy overloaded (bname, tm) defs =
    1.89 @@ -300,14 +253,13 @@
    1.90       [Pretty.str c, Pretty.str " ::", Pretty.brk 1,
    1.91        Pretty.quote (Pretty.typ pp (Type.freeze_type T))];
    1.92  
    1.93 -    val _ = no_vars pp tm;
    1.94      val name = Sign.full_name thy bname;
    1.95 -    val (const, rhs) = dest_def pp tm handle TERM (msg, _) => error msg;
    1.96 +    val (lhs_const, rhs) = Sign.cert_def pp tm;
    1.97      val rhs_consts = fold_aterms (fn Const const => insert (op =) const | _ => I) rhs [];
    1.98 -    val _ = check_overloading thy overloaded const;
    1.99 +    val _ = check_overloading thy overloaded lhs_const;
   1.100    in
   1.101      defs |> Defs.define (Sign.the_const_type thy)
   1.102 -      name (prep_const thy const) (map (prep_const thy) rhs_consts)
   1.103 +      name (prep_const thy lhs_const) (map (prep_const thy) rhs_consts)
   1.104    end
   1.105    handle ERROR msg => cat_error msg (Pretty.string_of (Pretty.block
   1.106     [Pretty.str ("The error(s) above occurred in definition " ^ quote bname ^ ":"),
   1.107 @@ -345,7 +297,7 @@
   1.108      fun specify (c, T) =
   1.109        Defs.define (Sign.the_const_type thy) (c ^ " axiom") (prep_const thy (c, T)) [];
   1.110      val finalize = specify o check_overloading thy overloaded o
   1.111 -      const_of o no_vars (Sign.pp thy) o prep_term thy;
   1.112 +      const_of o Sign.no_vars (Sign.pp thy) o prep_term thy;
   1.113    in thy |> map_defs (fold finalize args) end;
   1.114  
   1.115  in