src/CCL/Wfd.thy
changeset 29264 4ea3358fac3f
parent 27239 f2f42f9fa09d
child 29269 5c25a2012975
--- a/src/CCL/Wfd.thy	Wed Dec 31 00:01:51 2008 +0100
+++ b/src/CCL/Wfd.thy	Wed Dec 31 00:08:11 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      CCL/Wfd.thy
-    ID:         $Id$
     Author:     Martin Coen, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 *)
@@ -451,7 +450,7 @@
 
 fun is_rigid_prog t =
      case (Logic.strip_assums_concl t) of
-        (Const("Trueprop",_) $ (Const("mem",_) $ a $ _)) => (term_vars a = [])
+        (Const("Trueprop",_) $ (Const("mem",_) $ a $ _)) => null (Term.add_vars a [])
        | _ => false
 in