--- a/src/HOL/Nominal/nominal_inductive2.ML Wed Sep 09 14:47:41 2015 +0200
+++ b/src/HOL/Nominal/nominal_inductive2.ML Wed Sep 09 20:57:21 2015 +0200
@@ -44,11 +44,15 @@
th RS infer_instantiate ctxt [(#1 (dest_Var (Thm.term_of perm_boolI_pi)), pi)] perm_boolI;
fun mk_perm_bool_simproc names =
- Simplifier.simproc_global_i @{theory} "perm_bool" [@{term "perm pi x"}] (fn ctxt =>
- fn Const (@{const_name Nominal.perm}, _) $ _ $ t =>
- if member (op =) names (the_default "" (try (head_of #> dest_Const #> fst) t))
- then SOME perm_bool else NONE
- | _ => NONE);
+ Simplifier.make_simproc @{context} "perm_bool"
+ {lhss = [@{term "perm pi x"}],
+ proc = fn _ => fn _ => fn ct =>
+ (case Thm.term_of ct of
+ Const (@{const_name Nominal.perm}, _) $ _ $ t =>
+ if member (op =) names (the_default "" (try (head_of #> dest_Const #> fst) t))
+ then SOME perm_bool else NONE
+ | _ => NONE),
+ identifier = []};
fun transp ([] :: _) = []
| transp xs = map hd xs :: transp (map tl xs);