diff -r 1810b1ade437 -r 47ee18b6ae32 src/HOL/UNITY/SubstAx.thy
--- a/src/HOL/UNITY/SubstAx.thy	Mon Mar 01 12:30:55 2010 +0100
+++ b/src/HOL/UNITY/SubstAx.thy	Mon Mar 01 13:42:31 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/UNITY/SubstAx
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1998  University of Cambridge
 
@@ -10,11 +9,10 @@
 
 theory SubstAx imports WFair Constrains begin
 
-constdefs
-   Ensures :: "['a set, 'a set] => 'a program set"    (infixl "Ensures" 60)
+definition Ensures :: "['a set, 'a set] => 'a program set" (infixl "Ensures" 60) where
     "A Ensures B == {F. F \<in> (reachable F \<inter> A) ensures B}"
 
-   LeadsTo :: "['a set, 'a set] => 'a program set"    (infixl "LeadsTo" 60)
+definition LeadsTo :: "['a set, 'a set] => 'a program set" (infixl "LeadsTo" 60) where
     "A LeadsTo B == {F. F \<in> (reachable F \<inter> A) leadsTo B}"
 
 notation (xsymbols)