src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
changeset 60696 8304fb4fb823
parent 60367 e201bd8973db
child 60805 4cc49ead6e75
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Jul 08 19:28:43 2015 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Jul 08 21:33:00 2015 +0200
     1.3 @@ -947,7 +947,7 @@
     1.4      val U = TFree ("'u", @{sort type})
     1.5      val y = Free (yname, U)
     1.6      val f' = absdummy (U --> T') (Bound 0 $ y)
     1.7 -    val th' = Thm.certify_instantiate ctxt
     1.8 +    val th' = Thm.certify_instantiate ctxt'
     1.9        ([(dest_TVar uninst_T, U --> T'), (dest_TVar uninst_T', T')],
    1.10         [((fst (dest_Var f), (U --> T') --> T'), f')]) th
    1.11      val [th'] = Variable.export (Variable.declare_thm th' ctxt') ctxt [th']