# HG changeset patch
# User paulson
# Date 864204818 -7200
# Node ID 7203f4dbc0c54bab26f3f465649afd9a20aa95d3
# Parent  89e5f4163663a28b8bfe0aaa958657e99e460aa8
Removed rprod from the WF relation

diff -r 89e5f4163663 -r 7203f4dbc0c5 src/HOL/Subst/Unify.thy
--- a/src/HOL/Subst/Unify.thy	Wed May 21 10:53:02 1997 +0200
+++ b/src/HOL/Subst/Unify.thy	Wed May 21 10:53:38 1997 +0200
@@ -1,4 +1,5 @@
 (*  Title:      Subst/Unify
+    ID:         $Id$
     Author:     Konrad Slind, Cambridge University Computer Laboratory
     Copyright   1997  University of Cambridge
 
@@ -11,18 +12,17 @@
 
 consts
 
-   uterm_less :: "(('a uterm * 'a uterm) * ('a uterm * 'a uterm)) set"
-   unifyRel   :: "(('a uterm * 'a uterm) * ('a uterm * 'a uterm)) set"
-   unify      :: "'a uterm * 'a uterm => ('a * 'a uterm) subst"
+   unifyRel :: "(('a uterm * 'a uterm) * ('a uterm * 'a uterm)) set"
+   unify    :: "'a uterm * 'a uterm => ('a * 'a uterm) subst"
 
 defs
 
-  uterm_less_def "uterm_less == rprod (measure uterm_size) 
-                                      (measure uterm_size)"
-  
-  (* Termination relation for the Unify function *)
-  unifyRel_def  "unifyRel == inv_image  (finite_psubset ** uterm_less)
-                               (%(x,y). (vars_of x Un vars_of y, (x,y)))"
+  (*Termination relation for the Unify function:
+    --either the set of variables decreases
+    --or the first argument does (in fact, both do)
+  *)
+  unifyRel_def  "unifyRel == inv_image  (finite_psubset ** measure uterm_size)
+                               (%(M,N). (vars_of M Un vars_of N, M))"
 
 recdef unify "unifyRel"
   "unify(Const m, Const n)  = (if (m=n) then Subst[] else Fail)"