# HG changeset patch
# User wenzelm
# Date 938719388 -7200
# Node ID 22dc8b2455b827e6634062ee6dacdb7f8b5e12bd
# Parent  226ea33c7cd61cb8f3993317af6c8206a78dc5d2
local_def_i: typ option;
admit additional (fixed) type vars on rhs;

diff -r 226ea33c7cd6 -r 22dc8b2455b8 src/Pure/Isar/local_defs.ML
--- 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!*)