--- 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;