src/HOL/Tools/Function/induction_schema.ML
changeset 42361 23f352990944
parent 41418 b6dc60638be0
child 42495 1af81b70cf09
     1.1 --- a/src/HOL/Tools/Function/induction_schema.ML	Sat Apr 16 15:47:52 2011 +0200
     1.2 +++ b/src/HOL/Tools/Function/induction_schema.ML	Sat Apr 16 16:15:37 2011 +0200
     1.3 @@ -124,7 +124,7 @@
     1.4  
     1.5      val allqnames = fold (fn SchemeCase {qs, ...} => fold (insert (op =) o Free) qs) relevant_cases []
     1.6      val (Pbool :: xs') = map Free (Variable.variant_frees ctxt allqnames (("P", HOLogic.boolT) :: xs))
     1.7 -    val Cs' = map (Pattern.rewrite_term (ProofContext.theory_of ctxt) (filter_out (op aconv) (map Free xs ~~ xs')) []) Cs
     1.8 +    val Cs' = map (Pattern.rewrite_term (Proof_Context.theory_of ctxt) (filter_out (op aconv) (map Free xs ~~ xs')) []) Cs
     1.9  
    1.10      fun mk_case (SchemeCase {qs, oqnames, gs, lhs, ...}) =
    1.11        HOLogic.mk_Trueprop Pbool
    1.12 @@ -211,7 +211,7 @@
    1.13        SumTree.mk_inj T n (i + 1) (foldr1 HOLogic.mk_prod ts)
    1.14      val P_of = nth (map (fn (SchemeBranch { P, ... }) => P) branches)
    1.15  
    1.16 -    val thy = ProofContext.theory_of ctxt
    1.17 +    val thy = Proof_Context.theory_of ctxt
    1.18      val cert = cterm_of thy
    1.19  
    1.20      val P_comp = mk_ind_goal thy branches
    1.21 @@ -351,7 +351,7 @@
    1.22      val ([Rn,xn], ctxt'') = Variable.variant_fixes ["R","x"] ctxt'
    1.23      val R = Free (Rn, mk_relT ST)
    1.24      val x = Free (xn, ST)
    1.25 -    val cert = cterm_of (ProofContext.theory_of ctxt)
    1.26 +    val cert = cterm_of (Proof_Context.theory_of ctxt)
    1.27  
    1.28      val ineqss = mk_ineqs R scheme
    1.29        |> map (map (pairself (Thm.assume o cert)))