explicit close_derivation
authorhaftmann
Thu Oct 22 14:43:59 2009 +0200 (2009-10-22 ago)
changeset 330651cefea81ec4f
parent 33064 ba7ff3f9527a
child 33066 31e928d5653d
child 33069 d284306ea923
child 33075 f654dafa021e
child 33077 3c9cf88ec841
explicit close_derivation
src/Pure/axclass.ML
     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