# HG changeset patch
# User wenzelm
# Date 1139255950 -3600
# Node ID 947d3a694654e6b610c92496e40780d9612b8c16
# Parent  9228bbe9cd4e3a1b783afbc873cbe30cbfb4447d
moved no_vars to sign.ML;
removed dest_def (cf. Sign.cert_def);

diff -r 9228bbe9cd4e -r 947d3a694654 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Mon Feb 06 20:59:09 2006 +0100
+++ b/src/Pure/theory.ML	Mon Feb 06 20:59:10 2006 +0100
@@ -45,7 +45,6 @@
   val merge_refs: theory_ref * theory_ref -> theory_ref    (*exception TERM*)
   val requires: theory -> string -> string -> unit
   val assert_super: theory -> theory -> theory
-  val dest_def: Pretty.pp -> term -> (string * typ) * term
   val add_axioms: (bstring * string) list -> theory -> theory
   val add_axioms_i: (bstring * term) list -> theory -> theory
   val add_defs: bool -> (bstring * string) list -> theory -> theory
@@ -166,13 +165,6 @@
 fun err_in_axm msg name =
   cat_error msg ("The error(s) above occurred in axiom " ^ quote name);
 
-fun no_vars pp tm =
-  (case (Term.term_vars tm, Term.term_tvars tm) of
-    ([], []) => tm
-  | (ts, ixns) => error (Pretty.string_of (Pretty.block (Pretty.breaks
-      (Pretty.str "Illegal schematic variable(s) in term:" ::
-       map (Pretty.term pp) ts @ map (Pretty.typ pp o TVar) ixns)))));
-
 fun cert_axm thy (name, raw_tm) =
   let
     val pp = Sign.pp thy;
@@ -182,7 +174,7 @@
   in
     Term.no_dummy_patterns t handle TERM (msg, _) => error msg;
     assert (T = propT) "Term not of type prop";
-    (name, no_vars pp t)
+    (name, Sign.no_vars pp t)
   end;
 
 fun read_def_axm (thy, types, sorts) used (name, str) =
@@ -198,7 +190,7 @@
   let
     val pp = Sign.pp thy;
     val (t, _) = Sign.infer_types pp thy (K NONE) (K NONE) [] true ([pre_tm], propT);
-  in (name, no_vars pp t) end
+  in (name, Sign.no_vars pp t) end
   handle ERROR msg => err_in_axm msg name;
 
 
@@ -252,45 +244,6 @@
   end;
 
 
-(* dest_def *)
-
-fun dest_def pp tm =
-  let
-    fun err msg = raise TERM (msg, [tm]);
-
-    val (lhs, rhs) = Logic.dest_equals (Logic.strip_imp_concl tm)
-      handle TERM _ => err "Not a meta-equality (==)";
-    val (head, args) = Term.strip_comb (Pattern.beta_eta_contract lhs);
-    val (c, T) = Term.dest_Const head
-      handle TERM _ => err "Head of lhs not a constant";
-
-    fun dest_free (Free (x, _)) = x
-      | dest_free (Const ("TYPE", Type ("itself", [TFree (x, _)]))) = x
-      | dest_free _ = raise Match;
-
-    val show_terms = commas_quote o map (Pretty.string_of_term pp);
-    val show_frees = commas_quote o map dest_free;
-    val show_tfrees = commas_quote o map fst;
-
-    val lhs_nofrees = filter (not o can dest_free) args;
-    val lhs_dups = gen_duplicates (op aconv) args;
-    val rhs_extras = term_frees rhs |> fold (remove op aconv) args;
-    val rhs_extrasT = term_tfrees rhs |> fold (remove op =) (typ_tfrees T);
-  in
-    if not (null lhs_nofrees) then
-      err ("Non-variables as arguments on lhs: " ^ show_terms lhs_nofrees)
-    else if not (null lhs_dups) then
-      err ("Duplicate variables on lhs: " ^ show_frees lhs_dups)
-    else if not (null rhs_extras) then
-      err ("Extra variables on rhs: " ^ show_frees rhs_extras)
-    else if not (null rhs_extrasT) then
-      err ("Extra type variables on rhs: " ^ show_tfrees rhs_extrasT)
-    else if exists_Const (equal (c, T)) rhs then
-      err ("Constant to be defined occurs on rhs")
-    else ((c, T), rhs)
-  end;
-
-
 (* check_def *)
 
 fun check_def thy overloaded (bname, tm) defs =
@@ -300,14 +253,13 @@
      [Pretty.str c, Pretty.str " ::", Pretty.brk 1,
       Pretty.quote (Pretty.typ pp (Type.freeze_type T))];
 
-    val _ = no_vars pp tm;
     val name = Sign.full_name thy bname;
-    val (const, rhs) = dest_def pp tm handle TERM (msg, _) => error msg;
+    val (lhs_const, rhs) = Sign.cert_def pp tm;
     val rhs_consts = fold_aterms (fn Const const => insert (op =) const | _ => I) rhs [];
-    val _ = check_overloading thy overloaded const;
+    val _ = check_overloading thy overloaded lhs_const;
   in
     defs |> Defs.define (Sign.the_const_type thy)
-      name (prep_const thy const) (map (prep_const thy) rhs_consts)
+      name (prep_const thy lhs_const) (map (prep_const thy) rhs_consts)
   end
   handle ERROR msg => cat_error msg (Pretty.string_of (Pretty.block
    [Pretty.str ("The error(s) above occurred in definition " ^ quote bname ^ ":"),
@@ -345,7 +297,7 @@
     fun specify (c, T) =
       Defs.define (Sign.the_const_type thy) (c ^ " axiom") (prep_const thy (c, T)) [];
     val finalize = specify o check_overloading thy overloaded o
-      const_of o no_vars (Sign.pp thy) o prep_term thy;
+      const_of o Sign.no_vars (Sign.pp thy) o prep_term thy;
   in thy |> map_defs (fold finalize args) end;
 
 in