# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1272879788 -7200
# Node ID 8468be06bff1cb0588f663039cd00703bdc11a24
# Parent  0a04acc91ca149a636a776647e34a659c64700cd
Cheat support equations in new parser

diff -r 0a04acc91ca1 -r 8468be06bff1 Nominal/NewParser.thy
--- a/Nominal/NewParser.thy	Mon May 03 11:37:44 2010 +0200
+++ b/Nominal/NewParser.thy	Mon May 03 11:43:08 2010 +0200
@@ -508,11 +508,12 @@
   val lthy22 = Class.prove_instantiation_instance tac lthy21
   val fv_alpha_all = combine_fv_alpha_bns (qfv_ts_nobn, qfv_ts_bn) (alpha_ts_nobn, qalpha_ts_bn) bn_nos;
   val (names, supp_eq_t) = supp_eq fv_alpha_all;
-(*  val _ = warning "Support Equations";
-  val q_supp = HOLogic.conj_elims (Goal.prove lthy22 names [] supp_eq_t (fn _ => supp_eq_tac q_induct q_fv q_perm q_eq_iff lthy22 1)) handle _ => [];
-  val lthy23 = note_suffix "supp" q_supp lthy22;*)
+  val _ = warning "Support Equations";
+  (*supp_eq_tac q_induct q_fv q_perm q_eq_iff lthy22 1*)
+  val q_supp = HOLogic.conj_elims (Goal.prove lthy22 names [] supp_eq_t (fn _ => Skip_Proof.cheat_tac thy)) handle _ => [];
+  val lthy23 = note_suffix "supp" q_supp lthy22;
 in
-  (0, lthy22)
+  (0, lthy23)
 end
 *}