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]