src/HOL/Nominal/nominal_inductive.ML
changeset 32149 ef59550a55d3
parent 32035 8e77b6a250d5
child 32172 c4e55f30d527
     1.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Thu Jul 23 18:44:08 2009 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Thu Jul 23 18:44:09 2009 +0200
     1.3 @@ -403,7 +403,7 @@
     1.4            cut_facts_tac [th] 1 THEN REPEAT (etac conjE 1) THEN
     1.5            REPEAT (REPEAT (resolve_tac [conjI, impI] 1) THEN
     1.6              etac impE 1 THEN atac 1 THEN REPEAT (etac @{thm allE_Nil} 1) THEN
     1.7 -            asm_full_simp_tac (simpset_of thy) 1)
     1.8 +            asm_full_simp_tac (simpset_of ctxt) 1)
     1.9          end) |> singleton (ProofContext.export ctxt' ctxt);
    1.10  
    1.11      (** strong case analysis rule **)