--- a/etc/isar-keywords.el Thu Aug 30 09:47:46 2012 +0200
+++ b/etc/isar-keywords.el Thu Aug 30 09:47:46 2012 +0200
@@ -35,7 +35,6 @@
"bnf_codata"
"bnf_data"
"bnf_def"
- "bnf_of_typ"
"boogie_end"
"boogie_open"
"boogie_status"
@@ -471,7 +470,6 @@
"axioms"
"bnf_codata"
"bnf_data"
- "bnf_of_typ"
"boogie_end"
"boogie_open"
"bundle"
--- a/src/HOL/Codatatype/BNF_Comp.thy Thu Aug 30 09:47:46 2012 +0200
+++ b/src/HOL/Codatatype/BNF_Comp.thy Thu Aug 30 09:47:46 2012 +0200
@@ -9,8 +9,6 @@
theory BNF_Comp
imports Basic_BNFs
-keywords
- "bnf_of_typ" :: thy_decl
uses
"Tools/bnf_comp_tactics.ML"
"Tools/bnf_comp.ML"
--- a/src/HOL/Codatatype/Tools/bnf_comp.ML Thu Aug 30 09:47:46 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_comp.ML Thu Aug 30 09:47:46 2012 +0200
@@ -18,7 +18,6 @@
val bnf_of_typ: BNF_Def.const_policy -> binding -> (binding -> binding) ->
((string * sort) list list -> (string * sort) list) -> typ -> unfold_thms * Proof.context ->
(BNF_Def.BNF * (typ list * typ list)) * (unfold_thms * Proof.context)
- val bnf_of_typ_cmd: binding * string -> Proof.context -> Proof.context
val default_comp_sort: (string * sort) list list -> (string * sort) list
val normalize_bnfs: (int -> binding -> binding) -> ''a list list -> ''a list ->
(''a list list -> ''a list) -> BNF_Def.BNF list -> unfold_thms -> Proof.context ->
@@ -794,17 +793,4 @@
end
end;
-fun bnf_of_typ_cmd (b, rawT) lthy =
- let
- val ((bnf, (Ds, As)), (unfold, lthy')) =
- bnf_of_typ Smart_Inline b I default_comp_sort (Syntax.read_typ lthy rawT)
- (empty_unfold, lthy);
- in
- snd (seal_bnf unfold b Ds bnf lthy')
- end;
-
-val _ =
- Outer_Syntax.local_theory @{command_spec "bnf_of_typ"} "parse a type as composition of BNFs"
- (((Parse.binding --| Parse.$$$ "=") -- Parse.typ) >> bnf_of_typ_cmd);
-
end;
--- a/src/HOL/Codatatype/Tools/bnf_def.ML Thu Aug 30 09:47:46 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_def.ML Thu Aug 30 09:47:46 2012 +0200
@@ -507,8 +507,7 @@
val bnf_note_all = Attrib.setup_config_bool @{binding bnf_note_all} (K false);
fun user_policy ctxt =
- if Config.get ctxt bnf_note_all then Note_All_Facts_and_Axioms
- else Derive_All_Facts_Note_Most;
+ if Config.get ctxt bnf_note_all then Note_All_Facts_and_Axioms else Derive_All_Facts_Note_Most;
val smart_max_inline_size = 25; (*FUDGE*)