src/HOL/Tools/BNF/bnf_comp.ML
changeset 56254 a2dd9200854d
parent 56018 c3fc8692dbc1
child 56634 a001337c8d24
     1.1 --- a/src/HOL/Tools/BNF/bnf_comp.ML	Sat Mar 22 18:16:54 2014 +0100
     1.2 +++ b/src/HOL/Tools/BNF/bnf_comp.ML	Sat Mar 22 18:19:57 2014 +0100
     1.3 @@ -138,15 +138,15 @@
     1.4                     forall inner from inners. idead = dead  *)
     1.5  
     1.6      val (oDs, lthy1) = apfst (map TFree)
     1.7 -      (Variable.invent_types (replicate odead HOLogic.typeS) lthy);
     1.8 +      (Variable.invent_types (replicate odead @{sort type}) lthy);
     1.9      val (Dss, lthy2) = apfst (map (map TFree))
    1.10 -      (fold_map Variable.invent_types (map (fn n => replicate n HOLogic.typeS) ideads) lthy1);
    1.11 +      (fold_map Variable.invent_types (map (fn n => replicate n @{sort type}) ideads) lthy1);
    1.12      val (Ass, lthy3) = apfst (replicate ilive o map TFree)
    1.13 -      (Variable.invent_types (replicate ilive HOLogic.typeS) lthy2);
    1.14 +      (Variable.invent_types (replicate ilive @{sort type}) lthy2);
    1.15      val As = if ilive > 0 then hd Ass else [];
    1.16      val Ass_repl = replicate olive As;
    1.17      val (Bs, names_lthy) = apfst (map TFree)
    1.18 -      (Variable.invent_types (replicate ilive HOLogic.typeS) lthy3);
    1.19 +      (Variable.invent_types (replicate ilive @{sort type}) lthy3);
    1.20      val Bss_repl = replicate olive Bs;
    1.21  
    1.22      val ((((fs', Qs'), Asets), xs), _) = names_lthy
    1.23 @@ -363,11 +363,11 @@
    1.24      (* TODO: check 0 < n <= live *)
    1.25  
    1.26      val (Ds, lthy1) = apfst (map TFree)
    1.27 -      (Variable.invent_types (replicate dead HOLogic.typeS) lthy);
    1.28 +      (Variable.invent_types (replicate dead @{sort type}) lthy);
    1.29      val ((killedAs, As), lthy2) = apfst (`(take n) o map TFree)
    1.30 -      (Variable.invent_types (replicate live HOLogic.typeS) lthy1);
    1.31 +      (Variable.invent_types (replicate live @{sort type}) lthy1);
    1.32      val (Bs, _(*lthy3*)) = apfst (append killedAs o map TFree)
    1.33 -      (Variable.invent_types (replicate (live - n) HOLogic.typeS) lthy2);
    1.34 +      (Variable.invent_types (replicate (live - n) @{sort type}) lthy2);
    1.35  
    1.36      val ((Asets, lives), _(*names_lthy*)) = lthy
    1.37        |> mk_Frees "A" (map HOLogic.mk_setT (drop n As))
    1.38 @@ -462,11 +462,11 @@
    1.39      (* TODO: check 0 < n *)
    1.40  
    1.41      val (Ds, lthy1) = apfst (map TFree)
    1.42 -      (Variable.invent_types (replicate dead HOLogic.typeS) lthy);
    1.43 +      (Variable.invent_types (replicate dead @{sort type}) lthy);
    1.44      val ((newAs, As), lthy2) = apfst (chop n o map TFree)
    1.45 -      (Variable.invent_types (replicate (n + live) HOLogic.typeS) lthy1);
    1.46 +      (Variable.invent_types (replicate (n + live) @{sort type}) lthy1);
    1.47      val ((newBs, Bs), _(*lthy3*)) = apfst (chop n o map TFree)
    1.48 -      (Variable.invent_types (replicate (n + live) HOLogic.typeS) lthy2);
    1.49 +      (Variable.invent_types (replicate (n + live) @{sort type}) lthy2);
    1.50  
    1.51      val (Asets, _(*names_lthy*)) = lthy
    1.52        |> mk_Frees "A" (map HOLogic.mk_setT (newAs @ As));
    1.53 @@ -553,11 +553,11 @@
    1.54      fun unpermute xs = permute_like_unique (op =) dest src xs;
    1.55  
    1.56      val (Ds, lthy1) = apfst (map TFree)
    1.57 -      (Variable.invent_types (replicate dead HOLogic.typeS) lthy);
    1.58 +      (Variable.invent_types (replicate dead @{sort type}) lthy);
    1.59      val (As, lthy2) = apfst (map TFree)
    1.60 -      (Variable.invent_types (replicate live HOLogic.typeS) lthy1);
    1.61 +      (Variable.invent_types (replicate live @{sort type}) lthy1);
    1.62      val (Bs, _(*lthy3*)) = apfst (map TFree)
    1.63 -      (Variable.invent_types (replicate live HOLogic.typeS) lthy2);
    1.64 +      (Variable.invent_types (replicate live @{sort type}) lthy2);
    1.65  
    1.66      val (Asets, _(*names_lthy*)) = lthy
    1.67        |> mk_Frees "A" (map HOLogic.mk_setT (permute As));
    1.68 @@ -757,9 +757,9 @@
    1.69      val nwits = nwits_of_bnf bnf;
    1.70  
    1.71      val (As, lthy1) = apfst (map TFree)
    1.72 -      (Variable.invent_types (replicate live HOLogic.typeS) (fold Variable.declare_typ Ds lthy));
    1.73 +      (Variable.invent_types (replicate live @{sort type}) (fold Variable.declare_typ Ds lthy));
    1.74      val (Bs, _) = apfst (map TFree)
    1.75 -      (Variable.invent_types (replicate live HOLogic.typeS) lthy1);
    1.76 +      (Variable.invent_types (replicate live @{sort type}) lthy1);
    1.77  
    1.78      val (((fs, fs'), (Rs, Rs')), _(*names_lthy*)) = lthy
    1.79        |> mk_Frees' "f" (map2 (curry op -->) As Bs)