src/Pure/proofterm.ML
changeset 43329 84472e198515
parent 43326 47cf4bc789aa
child 43761 e72ba84ae58f
     1.1 --- a/src/Pure/proofterm.ML	Wed Jun 08 22:16:21 2011 +0200
     1.2 +++ b/src/Pure/proofterm.ML	Thu Jun 09 20:22:22 2011 +0200
     1.3 @@ -952,7 +952,7 @@
     1.4  
     1.5  fun canonical_instance typs =
     1.6    let
     1.7 -    val names = Name.invents Name.context Name.aT (length typs);
     1.8 +    val names = Name.invent Name.context Name.aT (length typs);
     1.9      val instT = map2 (fn a => fn T => (((a, 0), []), Type.strip_sorts T)) names typs;
    1.10    in instantiate (instT, []) end;
    1.11