# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1272432448 -7200
# Node ID 90758c187861c5ace002eb2986d0a010a357c383
# Parent  9ae5380c828a057f357d6a77ad07f125755fd82e
use sort at_base instead of at

diff -r 9ae5380c828a -r 90758c187861 Nominal/NewFv.thy
--- a/Nominal/NewFv.thy	Wed Apr 28 07:20:57 2010 +0200
+++ b/Nominal/NewFv.thy	Wed Apr 28 07:27:28 2010 +0200
@@ -26,7 +26,7 @@
 
 ML {*
 fun is_atom thy ty =
-  Sign.of_sort thy (ty, @{sort at})
+  Sign.of_sort thy (ty, @{sort at_base})
 
 fun is_atom_set thy (Type ("fun", [t, @{typ bool}])) = is_atom thy t
   | is_atom_set _ _ = false;
diff -r 9ae5380c828a -r 90758c187861 Nominal/NewParser.thy
--- a/Nominal/NewParser.thy	Wed Apr 28 07:20:57 2010 +0200
+++ b/Nominal/NewParser.thy	Wed Apr 28 07:27:28 2010 +0200
@@ -498,6 +498,7 @@
 
 
 typ exp_raw 
+typ pat_raw 
 thm exp_raw_fnclause_raw_fnclauses_raw_lrb_raw_lrbs_raw_pat_raw.induct[no_vars]
 thm b_fnclause_raw_b_fnclauses_raw_b_lrb_raw_b_lrbs_raw_b_pat_raw.simps[no_vars]
 thm permute_exp_raw_permute_fnclause_raw_permute_fnclauses_raw_permute_lrb_raw_permute_lrbs_raw_permute_pat_raw.simps[no_vars]