--- a/src/HOL/Tools/BNF/bnf_gfp.ML Mon Sep 08 23:09:04 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML Mon Sep 08 23:09:23 2014 +0200
@@ -70,15 +70,14 @@
val b_names = map Binding.name_of bs;
val b_name = mk_common_name b_names;
val b = Binding.name b_name;
- val mk_internal_b = Binding.name #> Binding.prefix true b_name #> Binding.conceal;
- fun mk_internal_bs name =
- map (fn b =>
- Binding.prefix true b_name (Binding.prefix_name (name ^ "_") b) |> Binding.conceal) bs;
+
+ fun mk_internal_of_b name =
+ Binding.prefix_name (name ^ "_") #> Binding.prefix true b_name #> Binding.conceal;
+ fun mk_internal_b name = mk_internal_of_b name b;
+ fun mk_internal_bs name = map (mk_internal_of_b name) bs;
val external_bs = map2 (Binding.prefix false) b_names bs
|> not note_all ? map Binding.conceal;
- (* TODO: check if m, n, etc., are sane *)
-
val deads = fold (union (op =)) Dss resDs;
val names_lthy = fold Variable.declare_typ deads lthy;
val passives = map fst (subtract (op = o apsnd TFree) deads resBs);