--- 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
@@ -288,18 +288,6 @@
(bnf', (unfold', lthy'))
end;
-fun clean_compose_bnf_cmd (outer, inners) lthy =
- let
- val outer = the (bnf_of lthy outer)
- val inners = map (the o bnf_of lthy) inners
- val b = name_of_bnf outer
- |> Binding.prefix_name compN
- |> Binding.suffix_name ("_" ^ implode (map (Binding.name_of o name_of_bnf) inners));
- in
- (snd o snd) (clean_compose_bnf Dont_Inline I b outer inners
- (empty_unfold, lthy))
- end;
-
(* Killing live variables *)
fun killN_bnf qualify n bnf (unfold, lthy) = if n = 0 then (bnf, (unfold, lthy)) else
@@ -406,9 +394,6 @@
(bnf', (unfold', lthy'))
end;
-fun killN_bnf_cmd (n, raw_bnf) lthy =
- (snd o snd) (killN_bnf I n (the (bnf_of lthy raw_bnf)) (empty_unfold, lthy));
-
(* Adding dummy live variables *)
fun liftN_bnf qualify n bnf (unfold, lthy) = if n = 0 then (bnf, (unfold, lthy)) else
@@ -505,9 +490,6 @@
(bnf', (unfold', lthy'))
end;
-fun liftN_bnf_cmd (n, raw_bnf) lthy =
- (snd o snd) (liftN_bnf I n (the (bnf_of lthy raw_bnf)) (empty_unfold, lthy));
-
(* Changing the order of live variables *)
fun permute_bnf qualify src dest bnf (unfold, lthy) = if src = dest then (bnf, (unfold, lthy)) else
@@ -596,10 +578,6 @@
(bnf', (unfold', lthy'))
end;
-fun permute_bnf_cmd ((src, dest), raw_bnf) lthy =
- (snd o snd) (permute_bnf I src dest (the (bnf_of lthy raw_bnf))
- (empty_unfold, lthy));
-
(* Composition pipeline *)
fun permute_and_kill qualify n src dest bnf =
@@ -662,12 +640,6 @@
apfst (rpair (Ds, As)) (clean_compose_bnf const_policy I b outer inners' (unfold', lthy'))
end;
-fun compose_bnf_cmd (((((b, outer), inners), oDs), Dss), Ass) lthy = (snd o snd)
- (compose_bnf Dont_Inline I b default_comp_sort (the (bnf_of lthy outer))
- (map (the o bnf_of lthy) inners)
- (map (Syntax.read_typ lthy) oDs) (map (map (Syntax.read_typ lthy)) Dss)
- (map (map (Syntax.read_typ lthy)) Ass) (empty_unfold, lthy));
-
(* Hide the type of the bound (optimization) and unfold the definitions (nicer to the user) *)
fun seal_bnf unfold b Ds bnf lthy =
@@ -755,8 +727,7 @@
val rel_unfold = Local_Defs.unfold lthy'
(map unfold_defs (filter_refl (rel_unfolds_of unfold))) rel_def;
- val unfold_defs'' =
- unfold_defs' o (Local_Defs.unfold lthy' (filter_refl [rel_def_of_bnf bnf']));
+ val unfold_defs'' = unfold_defs' o Local_Defs.unfold lthy' (filter_refl [rel_def_of_bnf bnf']);
val pred_def = unfold_defs'' (pred_def_of_bnf bnf' RS abs_pred_sym_pred_abs);
val pred_unfold = Local_Defs.unfold lthy'