src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
changeset 56239 17df7145a871
parent 55440 721b4561007a
child 56245 84fc7dfa3cd4
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Fri Mar 21 08:13:23 2014 +0100
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Fri Mar 21 10:45:03 2014 +0100
     1.3 @@ -1212,7 +1212,7 @@
     1.4      val constname = "quickcheck"
     1.5      val full_constname = Sign.full_bname thy constname
     1.6      val constT = map snd vs' ---> @{typ bool}
     1.7 -    val thy1 = Sign.add_consts_i [(Binding.name constname, constT, NoSyn)] thy
     1.8 +    val thy1 = Sign.add_consts [(Binding.name constname, constT, NoSyn)] thy
     1.9      val const = Const (full_constname, constT)
    1.10      val t =
    1.11        Logic.list_implies