src/HOL/Tools/old_primrec.ML
changeset 35845 e5980f0ad025
parent 35756 cfde251d03a5
child 36610 bafd82950e24
     1.1 --- a/src/HOL/Tools/old_primrec.ML	Sat Mar 20 02:23:41 2010 +0100
     1.2 +++ b/src/HOL/Tools/old_primrec.ML	Sat Mar 20 17:33:11 2010 +0100
     1.3 @@ -35,7 +35,7 @@
     1.4  fun unify_consts thy cs intr_ts =
     1.5    (let
     1.6      fun varify t (i, ts) =
     1.7 -      let val t' = map_types (Logic.incr_tvar (i + 1)) (snd (Type.varify [] t))
     1.8 +      let val t' = map_types (Logic.incr_tvar (i + 1)) (snd (Type.varify_global [] t))
     1.9        in (maxidx_of_term t', t'::ts) end;
    1.10      val (i, cs') = fold_rev varify cs (~1, []);
    1.11      val (i', intr_ts') = fold_rev varify intr_ts (i, []);
    1.12 @@ -281,7 +281,7 @@
    1.13        thy'
    1.14        |> fold_map note ((map fst eqns ~~ atts) ~~ map single simps);
    1.15      val simps'' = maps snd simps';
    1.16 -    val lhss = map (Logic.varify o fst o Logic.dest_equals o snd) defs';
    1.17 +    val lhss = map (Logic.varify_global o fst o Logic.dest_equals o snd) defs';
    1.18    in
    1.19      thy''
    1.20      |> note (("simps",