src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
changeset 50056 72efd6b4038d
parent 48221 e0ed7fab0d09
child 51314 eac4bb5adbf9
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Mon Nov 12 23:24:40 2012 +0100
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Mon Nov 12 23:24:40 2012 +0100
     1.3 @@ -931,7 +931,7 @@
     1.4      let
     1.5        val f = (fst (strip_comb (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of th))))))
     1.6        val Type ("fun", [uninst_T, uninst_T']) = fastype_of f
     1.7 -      val ([tname, tname', uname, yname], ctxt') = Variable.add_fixes ["'t", "'t'", "'u", "y"] ctxt
     1.8 +      val ([_, tname', uname, yname], ctxt') = Variable.add_fixes ["'t", "'t'", "'u", "y"] ctxt
     1.9        val T' = TFree (tname', HOLogic.typeS)
    1.10        val U = TFree (uname, HOLogic.typeS)
    1.11        val y = Free (yname, U)