src/HOL/Tools/datatype_rep_proofs.ML
changeset 20071 8f3e1ddb50e6
parent 20046 9c8909fc5865
child 20820 58693343905f
     1.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Tue Jul 11 12:16:52 2006 +0200
     1.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Tue Jul 11 12:16:54 2006 +0200
     1.3 @@ -392,7 +392,7 @@
     1.4          fun mk_thm i =
     1.5            let
     1.6              val Ts = map (TFree o rpair HOLogic.typeS)
     1.7 -              (variantlist (replicate i "'t", used));
     1.8 +              (Name.variant_list used (replicate i "'t"));
     1.9              val f = Free ("f", Ts ---> U)
    1.10            in Goal.prove_global sign [] [] (Logic.mk_implies
    1.11              (HOLogic.mk_Trueprop (HOLogic.list_all