src/Pure/Isar/class_target.ML
changeset 36674 d95f39448121
parent 36672 bd7f659f7de5
child 37145 01aa36932739
child 37232 c10fb22a5e0c
     1.1 --- a/src/Pure/Isar/class_target.ML	Wed May 05 09:24:41 2010 +0200
     1.2 +++ b/src/Pure/Isar/class_target.ML	Wed May 05 09:24:42 2010 +0200
     1.3 @@ -151,8 +151,9 @@
     1.4  fun these_operations thy = maps (#operations o the_class_data thy) o ancestry thy;
     1.5  
     1.6  val base_morphism = #base_morph oo the_class_data;
     1.7 -fun morphism thy class = base_morphism thy class
     1.8 -  $> Element.eq_morphism thy (these_defs thy [class]);
     1.9 +fun morphism thy class = case Element.eq_morphism thy (these_defs thy [class])
    1.10 + of SOME eq_morph => base_morphism thy class $> eq_morph
    1.11 +  | NONE => base_morphism thy class;
    1.12  val export_morphism = #export_morph oo the_class_data;
    1.13  
    1.14  fun print_classes thy =
    1.15 @@ -202,12 +203,11 @@
    1.16        #> fold (curry Graph.add_edge class) sups;
    1.17    in ClassData.map add_class thy end;
    1.18  
    1.19 -fun activate_defs class thms thy =
    1.20 -  let
    1.21 -    val eq_morph = Element.eq_morphism thy thms;
    1.22 -    fun amend cls thy = Locale.amend_registration (cls, base_morphism thy cls)
    1.23 -      (eq_morph, true) (export_morphism thy cls) thy;
    1.24 -  in fold amend (heritage thy [class]) thy end;
    1.25 +fun activate_defs class thms thy = case Element.eq_morphism thy thms
    1.26 + of SOME eq_morph => fold (fn cls => fn thy =>
    1.27 +      Locale.amend_registration (cls, base_morphism thy cls)
    1.28 +        (eq_morph, true) (export_morphism thy cls) thy) (heritage thy [class]) thy
    1.29 +  | NONE => thy;
    1.30  
    1.31  fun register_operation class (c, (t, some_def)) thy =
    1.32    let
    1.33 @@ -223,7 +223,7 @@
    1.34        (fn (defs, operations) =>
    1.35          (fold cons (the_list some_def) defs,
    1.36            (c, (class, (ty', t'))) :: operations))
    1.37 -    |> is_some some_def ? activate_defs class (the_list some_def)
    1.38 +    |> activate_defs class (the_list some_def)
    1.39    end;
    1.40  
    1.41  fun register_subclass (sub, sup) some_dep_morph some_wit export thy =