renamed Drule.sort_triv to Thm.sort_triv (cf. more_thm.ML);
authorwenzelm
Thu Jul 02 21:26:18 2009 +0200 (2009-07-02)
changeset 31904a86896359ca4
parent 31903 c5221dbc40f6
child 31905 4263be178c8f
renamed Drule.sort_triv to Thm.sort_triv (cf. more_thm.ML);
src/Pure/Isar/class.ML
src/Pure/axclass.ML
src/Pure/drule.ML
src/Pure/more_thm.ML
     1.1 --- a/src/Pure/Isar/class.ML	Thu Jul 02 20:55:44 2009 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Thu Jul 02 21:26:18 2009 +0200
     1.3 @@ -90,7 +90,7 @@
     1.4      val sup_of_classes = map (snd o rules thy) sups;
     1.5      val loc_axiom_intros = map Drule.standard' (Locale.axioms_of thy class);
     1.6      val axclass_intro = #intro (AxClass.get_info thy class);
     1.7 -    val base_sort_trivs = Drule.sort_triv thy (aT, base_sort);
     1.8 +    val base_sort_trivs = Thm.sort_triv thy (aT, base_sort);
     1.9      val tac = REPEAT (SOMEGOAL
    1.10        (Tactic.match_tac (axclass_intro :: sup_of_classes
    1.11           @ loc_axiom_intros @ base_sort_trivs)
     2.1 --- a/src/Pure/axclass.ML	Thu Jul 02 20:55:44 2009 +0200
     2.2 +++ b/src/Pure/axclass.ML	Thu Jul 02 21:26:18 2009 +0200
     2.3 @@ -580,7 +580,7 @@
     2.4                | T as TVar (_, S) => insert (eq_fst op =) (T, S)
     2.5                | _ => I) typ [];
     2.6          val hyps = vars
     2.7 -          |> map (fn (T, S) => (T, Drule.sort_triv thy (T, S) ~~ S));
     2.8 +          |> map (fn (T, S) => (T, Thm.sort_triv thy (T, S) ~~ S));
     2.9          val ths = (typ, sort)
    2.10            |> Sorts.of_sort_derivation (Syntax.pp_global thy) (Sign.classes_of thy)
    2.11             {class_relation =
     3.1 --- a/src/Pure/drule.ML	Thu Jul 02 20:55:44 2009 +0200
     3.2 +++ b/src/Pure/drule.ML	Thu Jul 02 21:26:18 2009 +0200
     3.3 @@ -108,7 +108,6 @@
     3.4    val dummy_thm: thm
     3.5    val sort_constraintI: thm
     3.6    val sort_constraint_eq: thm
     3.7 -  val sort_triv: theory -> typ * sort -> thm list
     3.8    val unconstrainTs: thm -> thm
     3.9    val with_subgoal: int -> (thm -> thm) -> thm -> thm
    3.10    val comp_no_flatten: thm * int -> int -> thm -> thm
    3.11 @@ -209,15 +208,6 @@
    3.12  
    3.13  (* type classes and sorts *)
    3.14  
    3.15 -fun sort_triv thy (T, S) =
    3.16 -  let
    3.17 -    val certT = Thm.ctyp_of thy;
    3.18 -    val cT = certT T;
    3.19 -    fun class_triv c =
    3.20 -      Thm.class_triv thy c
    3.21 -      |> Thm.instantiate ([(certT (TVar ((Name.aT, 0), [c])), cT)], []);
    3.22 -  in map class_triv S end;
    3.23 -
    3.24  fun unconstrainTs th =
    3.25    fold (Thm.unconstrainT o Thm.ctyp_of (Thm.theory_of_thm th) o TVar)
    3.26      (Thm.fold_terms Term.add_tvars th []) th;
     4.1 --- a/src/Pure/more_thm.ML	Thu Jul 02 20:55:44 2009 +0200
     4.2 +++ b/src/Pure/more_thm.ML	Thu Jul 02 21:26:18 2009 +0200
     4.3 @@ -26,6 +26,7 @@
     4.4    val eq_thm_thy: thm * thm -> bool
     4.5    val eq_thm_prop: thm * thm -> bool
     4.6    val equiv_thm: thm * thm -> bool
     4.7 +  val sort_triv: theory -> typ * sort -> thm list
     4.8    val check_shyps: sort list -> thm -> thm
     4.9    val is_dummy: thm -> bool
    4.10    val plain_prop_of: thm -> term
    4.11 @@ -168,7 +169,16 @@
    4.12    Pattern.equiv (Theory.merge (pairself Thm.theory_of_thm ths)) (pairself Thm.full_prop_of ths);
    4.13  
    4.14  
    4.15 -(* sort hypotheses *)
    4.16 +(* type classes and sorts *)
    4.17 +
    4.18 +fun sort_triv thy (T, S) =
    4.19 +  let
    4.20 +    val certT = Thm.ctyp_of thy;
    4.21 +    val cT = certT T;
    4.22 +    fun class_triv c =
    4.23 +      Thm.class_triv thy c
    4.24 +      |> Thm.instantiate ([(certT (TVar ((Name.aT, 0), [c])), cT)], []);
    4.25 +  in map class_triv S end;
    4.26  
    4.27  fun check_shyps sorts raw_th =
    4.28    let