# HG changeset patch
# User wenzelm
# Date 1553603132 -3600
# Node ID 6fa51a36b7f788e1331db958630fb33613118df0
# Parent  4ce5ce3a612bf3d5ec6ef6c82d189346fcd7eef7
export propositional status of consts;

diff -r 4ce5ce3a612b -r 6fa51a36b7f7 src/Pure/Isar/object_logic.ML
--- a/src/Pure/Isar/object_logic.ML	Mon Mar 25 21:46:37 2019 +0100
+++ b/src/Pure/Isar/object_logic.ML	Tue Mar 26 13:25:32 2019 +0100
@@ -17,6 +17,7 @@
   val ensure_propT: Proof.context -> term -> term
   val dest_judgment: Proof.context -> cterm -> cterm
   val judgment_conv: Proof.context -> conv -> conv
+  val is_propositional: Proof.context -> typ -> bool
   val elim_concl: Proof.context -> thm -> term option
   val declare_atomize: attribute
   val declare_rulify: attribute
@@ -146,6 +147,11 @@
   then Conv.arg_conv cv ct
   else raise CTERM ("judgment_conv", [ct]);
 
+fun is_propositional ctxt T =
+  T = propT orelse
+    let val x = Free (singleton (Variable.variant_frees ctxt []) ("x", T))
+    in can (fn () => Syntax.check_term ctxt (ensure_propT ctxt x)) () end;
+
 
 (* elimination rules *)
 
diff -r 4ce5ce3a612b -r 6fa51a36b7f7 src/Pure/Thy/export_theory.ML
--- a/src/Pure/Thy/export_theory.ML	Mon Mar 25 21:46:37 2019 +0100
+++ b/src/Pure/Thy/export_theory.ML	Tue Mar 26 13:25:32 2019 +0100
@@ -231,7 +231,7 @@
 
     val encode_const =
       let open XML.Encode Term_XML.Encode
-      in pair encode_syntax (pair (list string) (pair typ (option term))) end;
+      in pair encode_syntax (pair (list string) (pair typ (pair (option term) bool))) end;
 
     fun export_const c (T, abbrev) =
       let
@@ -239,7 +239,8 @@
         val T' = T |> Logic.unvarifyT_global |> Type.strip_sorts;
         val abbrev' = abbrev |> Option.map (standard_vars_global #> map_types Type.strip_sorts);
         val args = map (#1 o dest_TFree) (Consts.typargs (Sign.consts_of thy) (c, T'));
-      in encode_const (syntax, (args, (T', abbrev'))) end;
+        val propositional = Object_Logic.is_propositional thy_ctxt (Term.body_type T');
+      in encode_const (syntax, (args, (T', (abbrev', propositional)))) end;
 
     val _ =
       export_entities "consts" (SOME oo export_const) Sign.const_space
diff -r 4ce5ce3a612b -r 6fa51a36b7f7 src/Pure/Thy/export_theory.scala
--- a/src/Pure/Thy/export_theory.scala	Mon Mar 25 21:46:37 2019 +0100
+++ b/src/Pure/Thy/export_theory.scala	Tue Mar 26 13:25:32 2019 +0100
@@ -251,27 +251,29 @@
     syntax: Syntax,
     typargs: List[String],
     typ: Term.Typ,
-    abbrev: Option[Term.Term])
+    abbrev: Option[Term.Term],
+    propositional: Boolean)
   {
     def cache(cache: Term.Cache): Const =
       Const(entity.cache(cache),
         syntax,
         typargs.map(cache.string(_)),
         cache.typ(typ),
-        abbrev.map(cache.term(_)))
+        abbrev.map(cache.term(_)),
+        propositional)
   }
 
   def read_consts(provider: Export.Provider): List[Const] =
     provider.uncompressed_yxml(export_prefix + "consts").map((tree: XML.Tree) =>
       {
         val (entity, body) = decode_entity(Kind.CONST, tree)
-        val (syntax, (args, (typ, abbrev))) =
+        val (syntax, (args, (typ, (abbrev, propositional)))) =
         {
           import XML.Decode._
           pair(decode_syntax, pair(list(string),
-            pair(Term_XML.Decode.typ, option(Term_XML.Decode.term))))(body)
+            pair(Term_XML.Decode.typ, pair(option(Term_XML.Decode.term), bool))))(body)
         }
-        Const(entity, syntax, args, typ, abbrev)
+        Const(entity, syntax, args, typ, abbrev, propositional)
       })