src/Pure/axclass.ML
changeset 38383 1ad96229b455
parent 37249 8365cbc31349
child 39133 70d3915c92f0
equal deleted inserted replaced
38382:8b02c5bf1d0e 38383:1ad96229b455
   404     val prop = Logic.mk_equals (Const (c', T), t);
   404     val prop = Logic.mk_equals (Const (c', T), t);
   405     val b' = Thm.def_binding_optional (Binding.name (instance_name (tyco, c))) b;
   405     val b' = Thm.def_binding_optional (Binding.name (instance_name (tyco, c))) b;
   406   in
   406   in
   407     thy
   407     thy
   408     |> Thm.add_def false false (b', prop)
   408     |> Thm.add_def false false (b', prop)
   409     |>> (fn (_, thm) =>  Drule.transitive_thm OF [eq, thm])
   409     |>> (fn (_, thm) => Drule.transitive_thm OF [eq, thm])
   410   end;
   410   end;
   411 
   411 
   412 
   412 
   413 (* primitive rules *)
   413 (* primitive rules *)
   414 
   414