src/HOL/Nominal/nominal_inductive.ML
changeset 54991 1169c65e9698
parent 54983 2c57fc1f7a8c
child 56253 83b3c110f22d
     1.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Sat Jan 11 14:12:33 2014 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Sat Jan 11 14:34:11 2014 +0100
     1.3 @@ -580,7 +580,7 @@
     1.4        (map (map (rulify_term thy #> rpair [])) vc_compat)
     1.5    end;
     1.6  
     1.7 -fun prove_eqvt s xatoms ctxt =
     1.8 +fun prove_eqvt s xatoms ctxt =  (* FIXME ctxt should be called lthy *)
     1.9    let
    1.10      val thy = Proof_Context.theory_of ctxt;
    1.11      val ({names, ...}, {raw_induct, intrs, elims, ...}) =
    1.12 @@ -609,21 +609,21 @@
    1.13           atoms)
    1.14        end;
    1.15      val perm_pi_simp = Global_Theory.get_thms thy "perm_pi_simp";
    1.16 -    val eqvt_simpset = put_simpset HOL_basic_ss (Proof_Context.init_global thy) addsimps
    1.17 -      (NominalThmDecls.get_eqvt_thms ctxt @ perm_pi_simp) addsimprocs
    1.18 -      [mk_perm_bool_simproc names,
    1.19 -       NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun];
    1.20      val (([t], [pi]), ctxt') = ctxt |>
    1.21        Variable.import_terms false [concl_of raw_induct] ||>>
    1.22        Variable.variant_fixes ["pi"];
    1.23 +    val eqvt_simpset = put_simpset HOL_basic_ss ctxt' addsimps
    1.24 +      (NominalThmDecls.get_eqvt_thms ctxt' @ perm_pi_simp) addsimprocs
    1.25 +      [mk_perm_bool_simproc names,
    1.26 +       NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun];
    1.27      val ps = map (fst o HOLogic.dest_imp)
    1.28        (HOLogic.dest_conj (HOLogic.dest_Trueprop t));
    1.29 -    fun eqvt_tac ctxt'' pi (intr, vs) st =
    1.30 +    fun eqvt_tac pi (intr, vs) st =
    1.31        let
    1.32          fun eqvt_err s =
    1.33 -          let val ([t], ctxt''') = Variable.import_terms true [prop_of intr] ctxt
    1.34 +          let val ([t], ctxt'') = Variable.import_terms true [prop_of intr] ctxt'
    1.35            in error ("Could not prove equivariance for introduction rule\n" ^
    1.36 -            Syntax.string_of_term ctxt''' t ^ "\n" ^ s)
    1.37 +            Syntax.string_of_term ctxt'' t ^ "\n" ^ s)
    1.38            end;
    1.39          val res = SUBPROOF (fn {context = ctxt'', prems, params, ...} =>
    1.40            let
    1.41 @@ -639,7 +639,7 @@
    1.42        in
    1.43          case (Seq.pull res handle THM (s, _, _) => eqvt_err s) of
    1.44            NONE => eqvt_err ("Rule does not match goal\n" ^
    1.45 -            Syntax.string_of_term ctxt'' (hd (prems_of st)))
    1.46 +            Syntax.string_of_term ctxt' (hd (prems_of st)))
    1.47          | SOME (th, _) => Seq.single th
    1.48        end;
    1.49      val thss = map (fn atom =>
    1.50 @@ -654,9 +654,9 @@
    1.51                HOLogic.mk_imp (p, list_comb (h, ts1 @
    1.52                  map (NominalDatatype.mk_perm [] pi') ts2))
    1.53              end) ps)))
    1.54 -          (fn {context, ...} => EVERY (rtac raw_induct 1 :: map (fn intr_vs =>
    1.55 +          (fn _ => EVERY (rtac raw_induct 1 :: map (fn intr_vs =>
    1.56                full_simp_tac eqvt_simpset 1 THEN
    1.57 -              eqvt_tac context pi' intr_vs) intrs')) |>
    1.58 +              eqvt_tac pi' intr_vs) intrs')) |>
    1.59            singleton (Proof_Context.export ctxt' ctxt)))
    1.60        end) atoms
    1.61    in