# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1272701665 -3600
# Node ID 2ceec1b4b015c333659b7f82bfc4e51fc251c2bb
# Parent  233bb805a4df2875cfe4e7f872eea21ab6ea9b45
tuned

diff -r 233bb805a4df -r 2ceec1b4b015 Nominal/NewParser.thy
--- a/Nominal/NewParser.thy	Fri Apr 30 16:31:43 2010 +0100
+++ b/Nominal/NewParser.thy	Sat May 01 09:14:25 2010 +0100
@@ -519,7 +519,7 @@
 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]
 thm fv_exp_raw.simps fv_fnclause_raw.simps fv_fnclauses_raw.simps fv_lrb_raw.simps fv_lrbs_raw.simps fv_pat_raw.simps fv_b_lrbs_raw.simps fv_b_pat_raw.simps fv_b_fnclauses_raw.simps fv_b_lrb_raw.simps fv_b_fnclause_raw.simps
-thm alpha_exp_raw_alpha_fnclause_raw_alpha_fnclauses_raw_alpha_lrb_raw_alpha_lrbs_raw_alpha_pat_raw_alpha_b_lrbs_raw_alpha_b_pat_raw_alpha_b_fnclauses_raw_alpha_b_lrb_raw_alpha_b_fnclause_raw.intros
+thm alpha_exp_raw_alpha_fnclause_raw_alpha_fnclauses_raw_alpha_lrb_raw_alpha_lrbs_raw_alpha_pat_raw_alpha_b_lrbs_raw_alpha_b_pat_raw_alpha_b_fnclauses_raw_alpha_b_lrb_raw_alpha_b_fnclause_raw.intros[no_vars]
 
 nominal_datatype ty =
   Var "name"