src/Pure/axclass.ML
changeset 33065 1cefea81ec4f
parent 32966 5b21661fe618
child 33172 61ee96bc9895
     1.1 --- a/src/Pure/axclass.ML	Thu Oct 22 14:08:01 2009 +0200
     1.2 +++ b/src/Pure/axclass.ML	Thu Oct 22 14:43:59 2009 +0200
     1.3 @@ -364,12 +364,11 @@
     1.4        |> filter_out (fn (const, _) => can (get_inst_param thy) (const, t))
     1.5        |> (map o apsnd o map_atyps) (K T);
     1.6      val _ = map (Sign.certify_sort thy) Ss = Ss orelse err ();
     1.7 -    val th' = Drule.unconstrainTs th;
     1.8    in
     1.9      thy
    1.10      |> fold (snd oo declare_overloaded) missing_params
    1.11      |> Sign.primitive_arity (t, Ss, [c])
    1.12 -    |> put_arity ((t, Ss, c), th')
    1.13 +    |> put_arity ((t, Ss, c), Thm.close_derivation (Drule.unconstrainTs th))
    1.14    end;
    1.15  
    1.16