export shyps as regular typargs;
authorwenzelm
Mon Aug 06 11:06:43 2018 +0200 (11 months ago)
changeset 68727ec0b2833cfc4
parent 68726 782d6b89fb19
child 68740 682ff0e84387
export shyps as regular typargs;
src/Pure/Thy/export_theory.ML
src/Pure/drule.ML
     1.1 --- a/src/Pure/Thy/export_theory.ML	Sun Aug 05 20:32:18 2018 +0200
     1.2 +++ b/src/Pure/Thy/export_theory.ML	Mon Aug 06 11:06:43 2018 +0200
     1.3 @@ -127,28 +127,33 @@
     1.4  
     1.5      (* axioms and facts *)
     1.6  
     1.7 -    val standard_prop_of =
     1.8 -      Thm.transfer thy #>
     1.9 -      Thm.check_hyps (Context.Theory thy) #>
    1.10 -      Drule.sort_constraint_intr_shyps #>
    1.11 -      Thm.full_prop_of #>
    1.12 -      Term_Subst.zero_var_indexes;
    1.13 +    fun standard_prop_of raw_thm =
    1.14 +      let
    1.15 +        val thm = raw_thm
    1.16 +          |> Thm.transfer thy
    1.17 +          |> Thm.check_hyps (Context.Theory thy)
    1.18 +          |> Thm.strip_shyps;
    1.19 +        val prop = thm
    1.20 +          |> Thm.full_prop_of
    1.21 +          |> Term_Subst.zero_var_indexes;
    1.22 +      in (Thm.extra_shyps thm, prop) end;
    1.23  
    1.24 -    fun encode_prop prop =
    1.25 +    fun encode_prop (Ss, prop) =
    1.26        let
    1.27          val prop' = Logic.unvarify_global (named_bounds prop);
    1.28          val typargs = rev (Term.add_tfrees prop' []);
    1.29 +        val sorts = Name.invent (Name.make_context (map #1 typargs)) Name.aT (length Ss) ~~ Ss;
    1.30          val args = rev (Term.add_frees prop' []);
    1.31 -        open XML.Encode Term_XML.Encode;
    1.32        in
    1.33 -        triple (list (pair string sort)) (list (pair string typ)) term
    1.34 -          (typargs, args, prop')
    1.35 +        (sorts @ typargs, args, prop') |>
    1.36 +          let open XML.Encode Term_XML.Encode
    1.37 +          in triple (list (pair string sort)) (list (pair string typ)) term end
    1.38        end;
    1.39  
    1.40      val encode_fact = XML.Encode.list encode_prop o map standard_prop_of;
    1.41  
    1.42      val _ =
    1.43 -      export_entities "axioms" (K (SOME o encode_prop)) Theory.axiom_space
    1.44 +      export_entities "axioms" (fn _ => fn t => SOME (encode_prop ([], t))) Theory.axiom_space
    1.45          (Theory.axioms_of thy);
    1.46      val _ =
    1.47        export_entities "facts" (K (SOME o encode_fact)) (Facts.space_of o Global_Theory.facts_of)
     2.1 --- a/src/Pure/drule.ML	Sun Aug 05 20:32:18 2018 +0200
     2.2 +++ b/src/Pure/drule.ML	Mon Aug 06 11:06:43 2018 +0200
     2.3 @@ -98,8 +98,6 @@
     2.4    val is_sort_constraint: term -> bool
     2.5    val sort_constraintI: thm
     2.6    val sort_constraint_eq: thm
     2.7 -  val sort_constraint_intr: indexname * sort -> thm -> thm
     2.8 -  val sort_constraint_intr_shyps: thm -> thm
     2.9    val with_subgoal: int -> (thm -> thm) -> thm -> thm
    2.10    val comp_no_flatten: thm * int -> int -> thm -> thm
    2.11    val rename_bvars: (string * string) list -> thm -> thm
    2.12 @@ -649,26 +647,6 @@
    2.13          (Thm.unvarify_global (Context.the_global_context ()) sort_constraintI)))
    2.14        (implies_intr_list [A, C] (Thm.assume A)));
    2.15  
    2.16 -val sort_constraint_eq' = Thm.symmetric sort_constraint_eq;
    2.17 -
    2.18 -fun sort_constraint_intr tvar thm =
    2.19 -  Thm.equal_elim
    2.20 -    (Thm.instantiate
    2.21 -      ([((("'a", 0), []), Thm.global_ctyp_of (Thm.theory_of_thm thm) (TVar tvar))],
    2.22 -       [((("A", 0), propT), Thm.cprop_of thm)])
    2.23 -      sort_constraint_eq') thm;
    2.24 -
    2.25 -fun sort_constraint_intr_shyps raw_thm =
    2.26 -  let val thm = Thm.strip_shyps raw_thm in
    2.27 -    (case Thm.extra_shyps thm of
    2.28 -      [] => thm
    2.29 -    | shyps =>
    2.30 -        let
    2.31 -          val names = Name.make_context (map #1 (Thm.fold_terms Term.add_tvar_names thm []));
    2.32 -          val constraints = map (rpair 0) (Name.invent names Name.aT (length shyps)) ~~ shyps;
    2.33 -        in Thm.strip_shyps (fold_rev sort_constraint_intr constraints thm) end)
    2.34 -  end;
    2.35 -
    2.36  end;
    2.37  
    2.38