src/Pure/Thy/export_theory.ML
changeset 69988 6fa51a36b7f7
parent 69784 24bbc4e30e5b
child 69992 bd3c10813cc4
     1.1 --- a/src/Pure/Thy/export_theory.ML	Mon Mar 25 21:46:37 2019 +0100
     1.2 +++ b/src/Pure/Thy/export_theory.ML	Tue Mar 26 13:25:32 2019 +0100
     1.3 @@ -231,7 +231,7 @@
     1.4  
     1.5      val encode_const =
     1.6        let open XML.Encode Term_XML.Encode
     1.7 -      in pair encode_syntax (pair (list string) (pair typ (option term))) end;
     1.8 +      in pair encode_syntax (pair (list string) (pair typ (pair (option term) bool))) end;
     1.9  
    1.10      fun export_const c (T, abbrev) =
    1.11        let
    1.12 @@ -239,7 +239,8 @@
    1.13          val T' = T |> Logic.unvarifyT_global |> Type.strip_sorts;
    1.14          val abbrev' = abbrev |> Option.map (standard_vars_global #> map_types Type.strip_sorts);
    1.15          val args = map (#1 o dest_TFree) (Consts.typargs (Sign.consts_of thy) (c, T'));
    1.16 -      in encode_const (syntax, (args, (T', abbrev'))) end;
    1.17 +        val propositional = Object_Logic.is_propositional thy_ctxt (Term.body_type T');
    1.18 +      in encode_const (syntax, (args, (T', (abbrev', propositional)))) end;
    1.19  
    1.20      val _ =
    1.21        export_entities "consts" (SOME oo export_const) Sign.const_space