src/Pure/Isar/local_defs.ML
changeset 7667 22dc8b2455b8
parent 7502 257dd7777676
child 8092 badbfb6ceac0
--- a/src/Pure/Isar/local_defs.ML	Thu Sep 30 21:22:26 1999 +0200
+++ b/src/Pure/Isar/local_defs.ML	Thu Sep 30 21:23:08 1999 +0200
@@ -10,7 +10,7 @@
   val def: string -> Proof.context attribute list
     -> (string * string option) *  (string * string list) -> Proof.state -> Proof.state
   val def_i: string -> Proof.context attribute list
-    -> (string * typ) * (term * term list) -> Proof.state -> Proof.state
+    -> (string * typ option) * (term * term list) -> Proof.state -> Proof.state
 end;
 
 structure LocalDefs: LOCAL_DEFS =
@@ -33,10 +33,9 @@
     val lhs = ProofContext.cert_term ctxt' (Free (x, T));
     val eq = Logic.mk_equals (lhs, rhs);
   in
-    if lhs mem Term.add_term_frees (rhs, []) then
-      err "lhs occurs on rhs"
-    else if not (Term.term_tfrees rhs subset Term.typ_tfrees T) then
-      err "extra type variables on rhs"
+    if lhs mem Term.add_term_frees (rhs, []) then err "lhs occurs on rhs"
+(* FIXME    else if not (Term.term_tfrees rhs subset Term.typ_tfrees T) then
+      err "extra type variables on rhs"  *)
     else ();
     state'
     |> match_binds [(raw_pats, raw_rhs)]   (*note: raw_rhs prepared twice!*)