# HG changeset patch
# User wenzelm
# Date 1007595984 -3600
# Node ID c9775847ed66a86b6b6b6c599b6254cc61ad57dc
# Parent  9b16f99fd7b91b98e047f18a3680591718f26a98
use Main;

diff -r 9b16f99fd7b9 -r c9775847ed66 src/HOL/Subst/AList.thy
--- a/src/HOL/Subst/AList.thy	Thu Dec 06 00:45:04 2001 +0100
+++ b/src/HOL/Subst/AList.thy	Thu Dec 06 00:46:24 2001 +0100
@@ -6,7 +6,7 @@
 Association lists.
 *)
 
-AList = List + 
+AList = Main +
 
 consts
   alist_rec  :: "[('a*'b)list, 'c, ['a, 'b, ('a*'b)list, 'c]=>'c] => 'c"
diff -r 9b16f99fd7b9 -r c9775847ed66 src/HOL/Subst/UTerm.thy
--- a/src/HOL/Subst/UTerm.thy	Thu Dec 06 00:45:04 2001 +0100
+++ b/src/HOL/Subst/UTerm.thy	Thu Dec 06 00:46:24 2001 +0100
@@ -7,7 +7,7 @@
 Binary trees with leaves that are constants or variables.
 *)
 
-UTerm = Finite + Datatype +
+UTerm = Main +
 
 datatype 'a uterm = Var ('a) 
                   | Const ('a)
diff -r 9b16f99fd7b9 -r c9775847ed66 src/HOL/Subst/Unify.thy
--- a/src/HOL/Subst/Unify.thy	Thu Dec 06 00:45:04 2001 +0100
+++ b/src/HOL/Subst/Unify.thy	Thu Dec 06 00:46:24 2001 +0100
@@ -6,7 +6,7 @@
 Unification algorithm
 *)
 
-Unify = Unifier + Recdef + Option +
+Unify = Unifier +
 
 consts