# HG changeset patch # User blanchet # Date 1376256957 -7200 # Node ID 1b62f05ab4fd1c76a9838835de4e1f68a9e37de6 # Parent 797362ce0c144c04e8009ffbd049fa73ebf2735b honor user tfree names diff -r 797362ce0c14 -r 1b62f05ab4fd src/HOL/BNF/Tools/bnf_gfp.ML --- a/src/HOL/BNF/Tools/bnf_gfp.ML Sat Aug 10 12:00:34 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML Sun Aug 11 23:35:57 2013 +0200 @@ -62,21 +62,23 @@ val live = live_of_bnf (hd bnfs); val n = length bnfs; (*active*) val ks = 1 upto n; - val m = live - n (*passive, if 0 don't generate a new BNF*); + val m = live - n; (*passive, if 0 don't generate a new BNF*) val ls = 1 upto m; - val b = Binding.name (mk_common_name (map Binding.name_of bs)); + val b_names = map Binding.name_of bs; + val b = Binding.name (mk_common_name b_names); (* 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); (* tvars *) val ((((((((passiveAs, activeAs), passiveBs), activeBs), passiveCs), activeCs), passiveXs), passiveYs), idxT) = names_lthy - |> mk_TFrees m + |> variant_tfrees passives ||>> mk_TFrees n - ||>> mk_TFrees m + ||>> variant_tfrees passives ||>> mk_TFrees n ||>> mk_TFrees m ||>> mk_TFrees n @@ -96,7 +98,7 @@ (* types *) val dead_poss = - map (fn T => if member (op =) deads (TFree T) then SOME (TFree T) else NONE) resBs; + map (fn x => if member (op =) deads (TFree x) then SOME (TFree x) else NONE) resBs; fun mk_param NONE passive = (hd passive, tl passive) | mk_param (SOME a) passive = (a, passive); val mk_params = fold_map mk_param dead_poss #> fst; @@ -232,7 +234,7 @@ (* derived thms *) - (*map g1 ... gm g(m+1) ... g(m+n) (map id ... id f(m+1) ... f(m+n) x)= + (*map g1 ... gm g(m+1) ... g(m+n) (map id ... id f(m+1) ... f(m+n) x) = map g1 ... gm (g(m+1) o f(m+1)) ... (g(m+n) o f(m+n)) x*) fun mk_map_comp_id x mapAsBs mapBsCs mapAsCs map_comp = let diff -r 797362ce0c14 -r 1b62f05ab4fd src/HOL/BNF/Tools/bnf_lfp.ML --- a/src/HOL/BNF/Tools/bnf_lfp.ML Sat Aug 10 12:00:34 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_lfp.ML Sun Aug 11 23:35:57 2013 +0200 @@ -34,19 +34,21 @@ val n = length bnfs; (*active*) val ks = 1 upto n; val m = live - n; (*passive, if 0 don't generate a new BNF*) - val b = Binding.name (mk_common_name (map Binding.name_of bs)); + val b_names = map Binding.name_of bs; + val b = Binding.name (mk_common_name b_names); (* 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); (* tvars *) val ((((((passiveAs, activeAs), passiveBs), activeBs), activeCs), passiveXs), passiveYs) = names_lthy - |> mk_TFrees m + |> variant_tfrees passives ||>> mk_TFrees n - ||>> mk_TFrees m + ||>> variant_tfrees passives ||>> mk_TFrees n ||>> mk_TFrees n ||>> mk_TFrees m @@ -63,7 +65,7 @@ (* types *) val dead_poss = - map (fn T => if member (op =) deads (TFree T) then SOME (TFree T) else NONE) resBs; + map (fn x => if member (op =) deads (TFree x) then SOME (TFree x) else NONE) resBs; fun mk_param NONE passive = (hd passive, tl passive) | mk_param (SOME a) passive = (a, passive); val mk_params = fold_map mk_param dead_poss #> fst; @@ -189,7 +191,7 @@ (* derived thms *) - (*map g1 ... gm g(m+1) ... g(m+n) (map id ... id f(m+1) ... f(m+n) x)= + (*map g1 ... gm g(m+1) ... g(m+n) (map id ... id f(m+1) ... f(m+n) x) = map g1 ... gm (g(m+1) o f(m+1)) ... (g(m+n) o f(m+n)) x*) fun mk_map_comp_id x mapAsBs mapBsCs mapAsCs map_comp = let