# HG changeset patch
# User haftmann
# Date 1465241326 -7200
# Node ID f59fd6cc935e02ee3b548528eb1ccce5ded476b0
# Parent  f82c0b803bda6d62c7f1943b52e6944b3f2a0347
tuned signature

diff -r f82c0b803bda -r f59fd6cc935e src/Doc/Codegen/Further.thy
--- a/src/Doc/Codegen/Further.thy	Mon Jun 06 21:28:46 2016 +0200
+++ b/src/Doc/Codegen/Further.thy	Mon Jun 06 21:28:46 2016 +0200
@@ -345,4 +345,3 @@
 \<close>
 
 end
-
diff -r f82c0b803bda -r f59fd6cc935e src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Mon Jun 06 21:28:46 2016 +0200
+++ b/src/Pure/Isar/code.ML	Mon Jun 06 21:28:46 2016 +0200
@@ -10,10 +10,8 @@
 sig
   (*constants*)
   val check_const: theory -> term -> string
-  val read_bare_const: theory -> string -> string * typ
   val read_const: theory -> string -> string
   val string_of_const: theory -> string -> string
-  val const_typ: theory -> string -> typ
   val args_number: theory -> string -> int
 
   (*constructor sets*)
@@ -21,12 +19,8 @@
     -> string * ((string * sort) list * (string * ((string * sort) list * typ list)) list)
 
   (*code equations and certificates*)
-  val mk_eqn: theory -> thm * bool -> thm * bool
-  val mk_eqn_liberal: theory -> thm -> (thm * bool) option
   val assert_eqn: theory -> thm * bool -> thm * bool
   val assert_abs_eqn: theory -> string option -> thm -> thm * string
-  val const_typ_eqn: theory -> thm -> string * typ
-  val expand_eta: theory -> int -> thm -> thm
   type cert
   val constrain_cert: theory -> sort list -> cert -> cert
   val conclude_cert: cert -> cert