src/Pure/Isar/class.ML
changeset 25209 bc21d8de18a9
parent 25195 62638dcafe38
child 25210 5b5659801257
     1.1 --- a/src/Pure/Isar/class.ML	Fri Oct 26 21:22:19 2007 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Fri Oct 26 21:22:20 2007 +0200
     1.3 @@ -397,16 +397,6 @@
     1.4  fun these_unchecks thy =
     1.5    maps (#unchecks o the_class_data thy) o ancestry thy;
     1.6  
     1.7 -fun sups_base_sort thy sort =
     1.8 -  let
     1.9 -    val sups = filter (is_class thy) sort
    1.10 -      |> Sign.minimize_sort thy;
    1.11 -    val base_sort = case sups
    1.12 -     of _ :: _ => maps (#base_sort o the_class_data thy) sups
    1.13 -          |> Sign.minimize_sort thy
    1.14 -      | [] => sort;
    1.15 -  in (sups, base_sort) end;
    1.16 -
    1.17  fun print_classes thy =
    1.18    let
    1.19      val ctxt = ProofContext.init thy;
    1.20 @@ -493,8 +483,7 @@
    1.21        | subst_aterm t = t;
    1.22      val subst_term = map_aterms subst_aterm #> map_types subst_typ;
    1.23    in
    1.24 -    Morphism.identity
    1.25 -    $> Morphism.term_morphism subst_term
    1.26 +    Morphism.term_morphism subst_term
    1.27      $> Morphism.typ_morphism subst_typ
    1.28    end;
    1.29  
    1.30 @@ -648,8 +637,7 @@
    1.31  
    1.32      (* check phase *)
    1.33      val typargs = Consts.typargs (ProofContext.consts_of ctxt);
    1.34 -    fun check_const (c, ty) (t, (_, idx)) =
    1.35 -      ((nth (typargs (c, ty)) idx), t);
    1.36 +    fun check_const (c, ty) (t, (_, typidx)) = ((nth (typargs (c, ty)) typidx), t);
    1.37      fun local_operation (c_ty as (c, _)) = AList.lookup (op =) operations c
    1.38        |> Option.map (check_const c_ty);
    1.39  
    1.40 @@ -662,13 +650,13 @@
    1.41    in
    1.42      ctxt
    1.43      |> fold (ProofContext.add_const_constraint o local_constraint) operations
    1.44 -    |> ClassSyntax.map (K (SOME {
    1.45 +    |> ClassSyntax.put (SOME {
    1.46          constraints = constraints,
    1.47          base_sort = base_sort,
    1.48          local_operation = local_operation,
    1.49          unchecks = unchecks,
    1.50          passed = false
    1.51 -      }))
    1.52 +      })
    1.53    end;
    1.54  
    1.55  fun refresh_syntax class ctxt =
    1.56 @@ -715,7 +703,6 @@
    1.57  
    1.58  fun sort_term_uncheck ts ctxt =
    1.59    let
    1.60 -    (*FIXME abbreviations*)
    1.61      val thy = ProofContext.theory_of ctxt;
    1.62      val unchecks = (#unchecks o the o ClassSyntax.get) ctxt;
    1.63      val ts' = if ! uncheck
    1.64 @@ -746,7 +733,11 @@
    1.65  fun gen_class_spec prep_class prep_expr process_expr thy raw_supclasses raw_includes_elems =
    1.66    let
    1.67      val supclasses = map (prep_class thy) raw_supclasses;
    1.68 -    val (sups, base_sort) = sups_base_sort thy supclasses;
    1.69 +    val sups = filter (is_class thy) supclasses;
    1.70 +    fun the_base_sort class = lookup_class_data thy class
    1.71 +      |> Option.map #base_sort
    1.72 +      |> the_default [class];
    1.73 +    val base_sort = Sign.minimize_sort thy (maps the_base_sort supclasses);
    1.74      val supsort = Sign.minimize_sort thy supclasses;
    1.75      val suplocales = map Locale.Locale sups;
    1.76      val (raw_elems, includes) = fold_rev (fn Locale.Elem e => apfst (cons e)