tuned signature
authorhaftmann
Mon, 06 Jun 2016 21:28:46 +0200
changeset 63241 f59fd6cc935e
parent 63240 f82c0b803bda
child 63242 1bc6816fd525
child 63244 9986559617ee
child 63249 d1693d7b0c01
tuned signature
src/Doc/Codegen/Further.thy
src/Pure/Isar/code.ML
--- 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
-
--- 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