src/HOLCF/Tools/Domain/domain_extender.ML
changeset 40017 575d3aa1f3c5
parent 40016 2eff1cbc1ccb
child 40019 05cda34d36e7
     1.1 --- a/src/HOLCF/Tools/Domain/domain_extender.ML	Thu Oct 14 13:28:31 2010 -0700
     1.2 +++ b/src/HOLCF/Tools/Domain/domain_extender.ML	Thu Oct 14 13:46:27 2010 -0700
     1.3 @@ -198,7 +198,7 @@
     1.4      val (take_rews, theorems_thy) =
     1.5          thy
     1.6            |> Domain_Theorems.comp_theorems (comp_dbind, eqs)
     1.7 -              (dbinds ~~ map snd eqs') iso_infos take_info constr_infos;
     1.8 +              (dbinds ~~ map snd eqs') take_info constr_infos;
     1.9    in
    1.10      theorems_thy
    1.11    end;