src/Pure/Isar/class.ML
changeset 57139 5e9507c002cc
parent 57119 f6d1f88021be
child 57140 26df5a93ec27
equal deleted inserted replaced
57138:7b3146180291 57139:5e9507c002cc
   357 
   357 
   358 fun global_const dangling_params class phi ((b, mx), rhs) thy =
   358 fun global_const dangling_params class phi ((b, mx), rhs) thy =
   359   let
   359   let
   360     val dangling_params' = map (Morphism.term phi) dangling_params;
   360     val dangling_params' = map (Morphism.term phi) dangling_params;
   361     val b' = Morphism.binding phi b;
   361     val b' = Morphism.binding phi b;
   362     val b_def = Morphism.binding phi (Binding.suffix_name "_dict" b');
   362     val b_def = Binding.suffix_name "_dict" b';
   363     val rhs' = Morphism.term phi rhs;
   363     val rhs' = Morphism.term phi rhs;
   364     val c' = Sign.full_name thy b';
   364     val c' = Sign.full_name thy b';
   365     val ty' = map Term.fastype_of dangling_params' ---> Term.fastype_of rhs';
   365     val ty' = map Term.fastype_of dangling_params' ---> Term.fastype_of rhs';
   366     val def_eq = Logic.mk_equals (list_comb (Const (c', ty'), dangling_params'), rhs')
   366     val def_eq = Logic.mk_equals (list_comb (Const (c', ty'), dangling_params'), rhs')
   367       |> map_types Type.strip_sorts;
   367       |> map_types Type.strip_sorts;