# HG changeset patch
# User wenzelm
# Date 1575397946 -3600
# Node ID d411d5c84a4b4fcb841b980ee91aaa5579bb30b1
# Parent  6f8422385878664969914060775067c414027143# Parent  2bc39c80a95dfc1251a195016a8ec167c2323681
merged

diff -r 6f8422385878 -r d411d5c84a4b src/Pure/Thy/export_theory.ML
--- a/src/Pure/Thy/export_theory.ML	Tue Dec 03 16:12:20 2019 +0100
+++ b/src/Pure/Thy/export_theory.ML	Tue Dec 03 19:32:26 2019 +0100
@@ -55,18 +55,6 @@
   (fold_types o fold_atyps) (fn TFree (a, S) => is_free used a ? insert (op =) (a, S) | _ => I);
 
 
-(* spec rules *)
-
-fun primrec_types ctxt const =
-  Spec_Rules.retrieve ctxt (Const const)
-  |> get_first
-    (#rough_classification #>
-      (fn Spec_Rules.Equational (Spec_Rules.Primrec types) => SOME (types, false)
-        | Spec_Rules.Equational (Spec_Rules.Primcorec types) => SOME (types, true)
-        | _ => NONE))
-  |> the_default ([], false);
-
-
 (* locales *)
 
 fun locale_content thy loc =
@@ -216,23 +204,19 @@
     val encode_term = Term_XML.Encode.term consts;
 
     val encode_const =
-      let open XML.Encode Term_XML.Encode in
-        pair encode_syntax
-          (pair (list string)
-            (pair typ (pair (option encode_term) (pair bool (pair (list string) bool)))))
-      end;
+      let open XML.Encode Term_XML.Encode
+      in pair encode_syntax (pair (list string) (pair typ (pair (option encode_term) bool))) end;
 
     fun export_const c (T, abbrev) =
       let
         val syntax = get_syntax_const thy_ctxt c;
         val U = Logic.unvarifyT_global T;
         val U0 = Type.strip_sorts U;
-        val recursion = primrec_types thy_ctxt (c, U);
         val abbrev' = abbrev
           |> Option.map (Proofterm.standard_vars_term Name.context #> map_types Type.strip_sorts);
         val args = map (#1 o dest_TFree) (Consts.typargs consts (c, U0));
         val propositional = Object_Logic.is_propositional thy_ctxt (Term.body_type U0);
-      in encode_const (syntax, (args, (U0, (abbrev', (propositional, recursion))))) end;
+      in encode_const (syntax, (args, (U0, (abbrev', propositional)))) end;
 
     val _ =
       export_entities "consts" (SOME oo export_const) Sign.const_space
diff -r 6f8422385878 -r d411d5c84a4b src/Pure/Thy/export_theory.scala
--- a/src/Pure/Thy/export_theory.scala	Tue Dec 03 16:12:20 2019 +0100
+++ b/src/Pure/Thy/export_theory.scala	Tue Dec 03 19:32:26 2019 +0100
@@ -284,9 +284,7 @@
     typargs: List[String],
     typ: Term.Typ,
     abbrev: Option[Term.Term],
-    propositional: Boolean,
-    primrec_types: List[String],
-    corecursive: Boolean)
+    propositional: Boolean)
   {
     def cache(cache: Term.Cache): Const =
       Const(entity.cache(cache),
@@ -294,25 +292,22 @@
         typargs.map(cache.string(_)),
         cache.typ(typ),
         abbrev.map(cache.term(_)),
-        propositional,
-        primrec_types.map(cache.string(_)),
-        corecursive)
+        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, (propositional, (primrec_types, corecursive)))))) =
+        val (syntax, (typargs, (typ, (abbrev, propositional)))) =
         {
           import XML.Decode._
           pair(decode_syntax,
             pair(list(string),
               pair(Term_XML.Decode.typ,
-                pair(option(Term_XML.Decode.term), pair(bool,
-                  pair(list(string), bool))))))(body)
+                pair(option(Term_XML.Decode.term), bool))))(body)
         }
-        Const(entity, syntax, args, typ, abbrev, propositional, primrec_types, corecursive)
+        Const(entity, syntax, typargs, typ, abbrev, propositional)
       })
 
 
diff -r 6f8422385878 -r d411d5c84a4b src/Pure/term.scala
--- a/src/Pure/term.scala	Tue Dec 03 16:12:20 2019 +0100
+++ b/src/Pure/term.scala	Tue Dec 03 19:32:26 2019 +0100
@@ -53,6 +53,13 @@
   val dummyT = Type("dummy")
 
   sealed abstract class Term
+  {
+    def head: Term =
+      this match {
+        case App(fun, _) => fun.head
+        case _ => this
+      }
+  }
   case class Const(name: String, typargs: List[Typ] = Nil) extends Term
   {
     override def toString: String =