src/Pure/Isar/class_target.ML
changeset 31599 97b4d289c646
parent 31249 d51d2a22a4f9
child 31635 8623244a50d5
     1.1 --- a/src/Pure/Isar/class_target.ML	Tue Jun 09 22:59:55 2009 +0200
     1.2 +++ b/src/Pure/Isar/class_target.ML	Tue Jun 09 22:59:55 2009 +0200
     1.3 @@ -127,22 +127,21 @@
     1.4  
     1.5  };
     1.6  
     1.7 -fun rep_class_data (ClassData data) = data;
     1.8 -fun mk_class_data ((consts, base_sort, base_morph, assm_intro, of_class, axiom),
     1.9 +fun make_class_data ((consts, base_sort, base_morph, assm_intro, of_class, axiom),
    1.10      (defs, operations)) =
    1.11    ClassData { consts = consts, base_sort = base_sort,
    1.12      base_morph = base_morph, assm_intro = assm_intro, of_class = of_class, axiom = axiom,
    1.13      defs = defs, operations = operations };
    1.14  fun map_class_data f (ClassData { consts, base_sort, base_morph, assm_intro,
    1.15      of_class, axiom, defs, operations }) =
    1.16 -  mk_class_data (f ((consts, base_sort, base_morph, assm_intro, of_class, axiom),
    1.17 +  make_class_data (f ((consts, base_sort, base_morph, assm_intro, of_class, axiom),
    1.18      (defs, operations)));
    1.19  fun merge_class_data _ (ClassData { consts = consts,
    1.20      base_sort = base_sort, base_morph = base_morph, assm_intro = assm_intro,
    1.21      of_class = of_class, axiom = axiom, defs = defs1, operations = operations1 },
    1.22    ClassData { consts = _, base_sort = _, base_morph = _, assm_intro = _,
    1.23      of_class = _, axiom = _, defs = defs2, operations = operations2 }) =
    1.24 -  mk_class_data ((consts, base_sort, base_morph, assm_intro, of_class, axiom),
    1.25 +  make_class_data ((consts, base_sort, base_morph, assm_intro, of_class, axiom),
    1.26      (Thm.merge_thms (defs1, defs2),
    1.27        AList.merge (op =) (K true) (operations1, operations2)));
    1.28  
    1.29 @@ -158,7 +157,9 @@
    1.30  
    1.31  (* queries *)
    1.32  
    1.33 -val lookup_class_data = Option.map rep_class_data oo try o Graph.get_node o ClassData.get;
    1.34 +fun lookup_class_data thy class = case try (Graph.get_node (ClassData.get thy)) class
    1.35 + of SOME (ClassData data) => SOME data
    1.36 +  | NONE => NONE;
    1.37  
    1.38  fun the_class_data thy class = case lookup_class_data thy class
    1.39   of NONE => error ("Undeclared class " ^ quote class)
    1.40 @@ -188,8 +189,8 @@
    1.41    in (axiom, of_class) end;
    1.42  
    1.43  fun all_assm_intros thy =
    1.44 -  Graph.fold (fn (_, (data, _)) => fold (insert Thm.eq_thm)
    1.45 -    ((the_list o #assm_intro o rep_class_data) data)) (ClassData.get thy) [];
    1.46 +  Graph.fold (fn (_, (ClassData { assm_intro, ... }, _)) => fold (insert Thm.eq_thm)
    1.47 +    (the_list assm_intro)) (ClassData.get thy) [];
    1.48  
    1.49  fun these_defs thy = maps (#defs o the_class_data thy) o ancestry thy;
    1.50  fun these_operations thy = maps (#operations o the_class_data thy) o ancestry thy;
    1.51 @@ -240,7 +241,7 @@
    1.52      val operations = map (fn (v_ty as (_, ty), (c, _)) =>
    1.53        (c, (class, (ty, Free v_ty)))) params;
    1.54      val add_class = Graph.new_node (class,
    1.55 -        mk_class_data (((map o pairself) fst params, base_sort,
    1.56 +        make_class_data (((map o pairself) fst params, base_sort,
    1.57            morph, assm_intro, of_class, axiom), ([], operations)))
    1.58        #> fold (curry Graph.add_edge class) sups;
    1.59    in ClassData.map add_class thy end;