# HG changeset patch
# User wenzelm
# Date 1565185773 -7200
# Node ID 59250a32811356003cea2ca0e9c1a1555dde2c70
# Parent  d4b5139eea34a135695282e2228db34f3c1fee35
clarified proofterms;

diff -r d4b5139eea34 -r 59250a328113 src/HOL/Tools/typedef.ML
--- a/src/HOL/Tools/typedef.ML	Wed Aug 07 15:48:52 2019 +0200
+++ b/src/HOL/Tools/typedef.ML	Wed Aug 07 15:49:33 2019 +0200
@@ -244,12 +244,12 @@
 
     fun typedef_result inhabited lthy1 =
       let
-        val typedef' = inhabited RS typedef;
-        fun make th = Goal.norm_result lthy1 (typedef' RS th);
-        val (((((((((((_, [type_definition]), Rep), Rep_inverse), Abs_inverse), Rep_inject),
-            Abs_inject), Rep_cases), Abs_cases), Rep_induct), Abs_induct), lthy2) = lthy1
-          |> Local_Theory.note ((type_definition_name, []), [typedef'])
-          ||>> note ((Rep_name, []), make @{thm type_definition.Rep})
+        val ((_, [type_definition]), lthy2) = lthy1
+          |> Local_Theory.note ((type_definition_name, []), [inhabited RS typedef]);
+        fun make th = Goal.norm_result lthy2 (type_definition RS th);
+        val (((((((((Rep, Rep_inverse), Abs_inverse), Rep_inject), Abs_inject), Rep_cases),
+            Abs_cases), Rep_induct), Abs_induct), lthy3) = lthy2
+          |> note ((Rep_name, []), make @{thm type_definition.Rep})
           ||>> note ((Binding.suffix_name "_inverse" Rep_name, []),
               make @{thm type_definition.Rep_inverse})
           ||>> note ((Binding.suffix_name "_inverse" Abs_name, []),
@@ -283,7 +283,7 @@
             Rep_inject = Rep_inject, Abs_inject = Abs_inject, Rep_cases = Rep_cases,
           Abs_cases = Abs_cases, Rep_induct = Rep_induct, Abs_induct = Abs_induct});
       in
-        lthy2
+        lthy3
         |> Local_Theory.declaration {syntax = false, pervasive = true}
           (fn phi => put_info full_name (transform_info phi info))
         |> Typedef_Plugin.data Plugin_Name.default_filter full_name
@@ -301,9 +301,7 @@
   let
     val ((goal, _, typedef_result), lthy') =
       prepare_typedef Syntax.check_term overloaded typ set opt_bindings lthy;
-    val inhabited =
-      Goal.prove lthy' [] [] goal (tac o #context)
-      |> Goal.norm_result lthy' |> Thm.close_derivation;
+    val inhabited = Goal.prove lthy' [] [] goal (tac o #context) |> Goal.norm_result lthy';
   in typedef_result inhabited lthy' end;
 
 fun add_typedef_global overloaded typ set opt_bindings tac =