src/HOL/Tools/Quickcheck/narrowing_generators.ML
changeset 51689 43a3465805dd
parent 51673 4dfa00e264d8
parent 51685 385ef6706252
child 55147 bce3dbc11f95
     1.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Wed Apr 10 18:51:21 2013 +0200
     1.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Wed Apr 10 19:14:47 2013 +0200
     1.3 @@ -93,7 +93,7 @@
     1.4      val ty = Type (tyco, map TFree vs);
     1.5      val cs = (map o apsnd o apsnd o map o map_atyps)
     1.6        (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_cs;
     1.7 -    val const = AxClass.param_of_inst thy (@{const_name partial_term_of}, tyco);
     1.8 +    val const = Axclass.param_of_inst thy (@{const_name partial_term_of}, tyco);
     1.9      val var_insts =
    1.10        map (SOME o Thm.cterm_of thy o Logic.unvarify_types_global o Logic.varify_global)
    1.11          [Free ("ty", Term.itselfT ty), @{term "Quickcheck_Narrowing.Narrowing_variable p tt"},