# HG changeset patch # User paulson # Date 953544247 -3600 # Node ID 7ffc94f2f42d7333a1098b42672fa72986bdb541 # Parent 581dfabf22dde9391c8192372b6dd31e5263538e now based on "Main", as it should be diff -r 581dfabf22dd -r 7ffc94f2f42d src/HOL/Lex/Prefix.thy --- a/src/HOL/Lex/Prefix.thy Mon Mar 20 10:23:24 2000 +0100 +++ b/src/HOL/Lex/Prefix.thy Mon Mar 20 10:24:07 2000 +0100 @@ -4,7 +4,7 @@ Copyright 1995 TUM *) -Prefix = List + +Prefix = Main + arities list :: (term)ord