merged
authorhuffman
Wed Aug 10 18:07:32 2011 -0700 (2011-08-10)
changeset 44143d282b3c5df7c
parent 44142 8e27e0177518
parent 44134 fa98623f1006
child 44144 74b3751ea271
merged
src/Pure/codegen.ML
src/Pure/old_term.ML
     1.1 --- a/src/FOL/IFOL.thy	Wed Aug 10 18:02:16 2011 -0700
     1.2 +++ b/src/FOL/IFOL.thy	Wed Aug 10 18:07:32 2011 -0700
     1.3 @@ -7,6 +7,7 @@
     1.4  theory IFOL
     1.5  imports Pure
     1.6  uses
     1.7 +  "~~/src/Tools/misc_legacy.ML"
     1.8    "~~/src/Provers/splitter.ML"
     1.9    "~~/src/Provers/hypsubst.ML"
    1.10    "~~/src/Tools/IsaPlanner/zipper.ML"
     2.1 --- a/src/FOL/IsaMakefile	Wed Aug 10 18:02:16 2011 -0700
     2.2 +++ b/src/FOL/IsaMakefile	Wed Aug 10 18:07:32 2011 -0700
     2.3 @@ -29,8 +29,9 @@
     2.4  
     2.5  $(OUT)/FOL: $(OUT)/Pure $(SRC)/Provers/blast.ML				\
     2.6    $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML			\
     2.7 -  $(SRC)/Tools/case_product.ML $(SRC)/Tools/IsaPlanner/zipper.ML	\
     2.8 -  $(SRC)/Tools/IsaPlanner/isand.ML $(SRC)/Tools/IsaPlanner/rw_tools.ML	\
     2.9 +  $(SRC)/Tools/case_product.ML $(SRC)/Tools/misc_legacy.ML		\
    2.10 +  $(SRC)/Tools/IsaPlanner/zipper.ML $(SRC)/Tools/IsaPlanner/isand.ML	\
    2.11 +  $(SRC)/Tools/IsaPlanner/rw_tools.ML					\
    2.12    $(SRC)/Tools/IsaPlanner/rw_inst.ML $(SRC)/Tools/eqsubst.ML		\
    2.13    $(SRC)/Provers/hypsubst.ML $(SRC)/Tools/induct.ML			\
    2.14    $(SRC)/Tools/intuitionistic.ML $(SRC)/Tools/atomize_elim.ML		\
     3.1 --- a/src/FOLP/IFOLP.thy	Wed Aug 10 18:02:16 2011 -0700
     3.2 +++ b/src/FOLP/IFOLP.thy	Wed Aug 10 18:07:32 2011 -0700
     3.3 @@ -7,7 +7,7 @@
     3.4  
     3.5  theory IFOLP
     3.6  imports Pure
     3.7 -uses ("hypsubst.ML") ("intprover.ML")
     3.8 +uses "~~/src/Tools/misc_legacy.ML" ("hypsubst.ML") ("intprover.ML")
     3.9  begin
    3.10  
    3.11  setup Pure_Thy.old_appl_syntax_setup
     4.1 --- a/src/FOLP/IsaMakefile	Wed Aug 10 18:02:16 2011 -0700
     4.2 +++ b/src/FOLP/IsaMakefile	Wed Aug 10 18:07:32 2011 -0700
     4.3 @@ -26,7 +26,7 @@
     4.4  	@cd $(SRC)/Pure; $(ISABELLE_TOOL) make Pure
     4.5  
     4.6  $(OUT)/FOLP: $(OUT)/Pure FOLP.thy IFOLP.thy ROOT.ML classical.ML	\
     4.7 -  hypsubst.ML intprover.ML simp.ML simpdata.ML
     4.8 +  hypsubst.ML intprover.ML simp.ML simpdata.ML $(SRC)/Tools/misc_legacy.ML
     4.9  	@$(ISABELLE_TOOL) usedir -b $(OUT)/Pure FOLP
    4.10  
    4.11  
     5.1 --- a/src/FOLP/simp.ML	Wed Aug 10 18:02:16 2011 -0700
     5.2 +++ b/src/FOLP/simp.ML	Wed Aug 10 18:07:32 2011 -0700
     5.3 @@ -155,21 +155,21 @@
     5.4  (*ccs contains the names of the constants possessing congruence rules*)
     5.5  fun add_hidden_vars ccs =
     5.6    let fun add_hvars tm hvars = case tm of
     5.7 -              Abs(_,_,body) => OldTerm.add_term_vars(body,hvars)
     5.8 +              Abs(_,_,body) => Misc_Legacy.add_term_vars(body,hvars)
     5.9              | _$_ => let val (f,args) = strip_comb tm
    5.10                       in case f of
    5.11                              Const(c,T) =>
    5.12                                  if member (op =) ccs c
    5.13                                  then fold_rev add_hvars args hvars
    5.14 -                                else OldTerm.add_term_vars (tm, hvars)
    5.15 -                          | _ => OldTerm.add_term_vars (tm, hvars)
    5.16 +                                else Misc_Legacy.add_term_vars (tm, hvars)
    5.17 +                          | _ => Misc_Legacy.add_term_vars (tm, hvars)
    5.18                       end
    5.19              | _ => hvars;
    5.20    in add_hvars end;
    5.21  
    5.22  fun add_new_asm_vars new_asms =
    5.23      let fun itf (tm, at) vars =
    5.24 -                if at then vars else OldTerm.add_term_vars(tm,vars)
    5.25 +                if at then vars else Misc_Legacy.add_term_vars(tm,vars)
    5.26          fun add_list(tm,al,vars) = let val (_,tml) = strip_comb tm
    5.27                  in if length(tml)=length(al)
    5.28                     then fold_rev itf (tml ~~ al) vars
    5.29 @@ -197,7 +197,7 @@
    5.30      val hvars = add_new_asm_vars new_asms (rhs,hvars)
    5.31      fun it_asms asm hvars =
    5.32          if atomic asm then add_new_asm_vars new_asms (asm,hvars)
    5.33 -        else OldTerm.add_term_frees(asm,hvars)
    5.34 +        else Misc_Legacy.add_term_frees(asm,hvars)
    5.35      val hvars = fold_rev it_asms asms hvars
    5.36      val hvs = map (#1 o dest_Var) hvars
    5.37      val refl1_tac = refl_tac 1
    5.38 @@ -543,7 +543,7 @@
    5.39  fun find_subst sg T =
    5.40  let fun find (thm::thms) =
    5.41          let val (Const(_,cT), va, vb) = dest_red(hd(prems_of thm));
    5.42 -            val [P] = subtract (op =) [va, vb] (OldTerm.add_term_vars (concl_of thm, []));
    5.43 +            val [P] = subtract (op =) [va, vb] (Misc_Legacy.add_term_vars (concl_of thm, []));
    5.44              val eqT::_ = binder_types cT
    5.45          in if Sign.typ_instance sg (T,eqT) then SOME(thm,va,vb,P)
    5.46             else find thms
     6.1 --- a/src/HOL/Decision_Procs/Cooper.thy	Wed Aug 10 18:02:16 2011 -0700
     6.2 +++ b/src/HOL/Decision_Procs/Cooper.thy	Wed Aug 10 18:07:32 2011 -0700
     6.3 @@ -1996,7 +1996,7 @@
     6.4    let
     6.5      val thy = Thm.theory_of_cterm ct;
     6.6      val t = Thm.term_of ct;
     6.7 -    val fs = OldTerm.term_frees t;
     6.8 +    val fs = Misc_Legacy.term_frees t;
     6.9      val bs = term_bools [] t;
    6.10      val vs = map_index swap fs;
    6.11      val ps = map_index swap bs;
     7.1 --- a/src/HOL/Decision_Procs/MIR.thy	Wed Aug 10 18:02:16 2011 -0700
     7.2 +++ b/src/HOL/Decision_Procs/MIR.thy	Wed Aug 10 18:07:32 2011 -0700
     7.3 @@ -5635,7 +5635,7 @@
     7.4    let 
     7.5      val thy = Thm.theory_of_cterm ct;
     7.6      val t = Thm.term_of ct;
     7.7 -    val fs = OldTerm.term_frees t;
     7.8 +    val fs = Misc_Legacy.term_frees t;
     7.9      val vs = map_index swap fs;
    7.10      val qe = if proofs then @{code mirlfrqe} else @{code mircfrqe};
    7.11      val t' = (term_of_fm vs o qe o fm_of_term vs) t;
     8.1 --- a/src/HOL/Decision_Procs/commutative_ring_tac.ML	Wed Aug 10 18:02:16 2011 -0700
     8.2 +++ b/src/HOL/Decision_Procs/commutative_ring_tac.ML	Wed Aug 10 18:07:32 2011 -0700
     8.3 @@ -68,7 +68,7 @@
     8.4  fun reif_eq thy (eq as Const(@{const_name HOL.eq}, Type("fun", [T, _])) $ lhs $ rhs) =
     8.5        if Sign.of_sort thy (T, cr_sort) then
     8.6          let
     8.7 -          val fs = OldTerm.term_frees eq;
     8.8 +          val fs = Misc_Legacy.term_frees eq;
     8.9            val cvs = cterm_of thy (HOLogic.mk_list T fs);
    8.10            val clhs = cterm_of thy (reif_polex T fs lhs);
    8.11            val crhs = cterm_of thy (reif_polex T fs rhs);
     9.1 --- a/src/HOL/Decision_Procs/cooper_tac.ML	Wed Aug 10 18:02:16 2011 -0700
     9.2 +++ b/src/HOL/Decision_Procs/cooper_tac.ML	Wed Aug 10 18:07:32 2011 -0700
     9.3 @@ -55,7 +55,7 @@
     9.4      val (fm',np) = List.foldr (fn ((x, T), (fm,n)) => mk_all ((x, T), (fm,n)))
     9.5        (List.foldr HOLogic.mk_imp c rhs, np) ps
     9.6      val (vs, _) = List.partition (fn t => q orelse (type_of t) = nT)
     9.7 -      (OldTerm.term_frees fm' @ OldTerm.term_vars fm');
     9.8 +      (Misc_Legacy.term_frees fm' @ Misc_Legacy.term_vars fm');
     9.9      val fm2 = List.foldr mk_all2 fm' vs
    9.10    in (fm2, np + length vs, length rhs) end;
    9.11  
    10.1 --- a/src/HOL/Decision_Procs/ferrack_tac.ML	Wed Aug 10 18:02:16 2011 -0700
    10.2 +++ b/src/HOL/Decision_Procs/ferrack_tac.ML	Wed Aug 10 18:07:32 2011 -0700
    10.3 @@ -61,7 +61,7 @@
    10.4      val (fm',np) =  List.foldr (fn ((x, T), (fm,n)) => mk_all ((x, T), (fm,n)))
    10.5        (List.foldr HOLogic.mk_imp c rhs, np) ps
    10.6      val (vs, _) = List.partition (fn t => q orelse (type_of t) = HOLogic.natT)
    10.7 -      (OldTerm.term_frees fm' @ OldTerm.term_vars fm');
    10.8 +      (Misc_Legacy.term_frees fm' @ Misc_Legacy.term_vars fm');
    10.9      val fm2 = List.foldr mk_all2 fm' vs
   10.10    in (fm2, np + length vs, length rhs) end;
   10.11  
    11.1 --- a/src/HOL/Decision_Procs/langford.ML	Wed Aug 10 18:02:16 2011 -0700
    11.2 +++ b/src/HOL/Decision_Procs/langford.ML	Wed Aug 10 18:07:32 2011 -0700
    11.3 @@ -113,7 +113,7 @@
    11.4    val eqI = instantiate' [] [SOME ll, SOME rr] @{thm iffI}
    11.5   in Thm.implies_elim (Thm.implies_elim eqI thl) thr |> mk_meta_eq end;
    11.6  
    11.7 -fun contains x ct = member (op aconv) (OldTerm.term_frees (term_of ct)) (term_of x);
    11.8 +fun contains x ct = member (op aconv) (Misc_Legacy.term_frees (term_of ct)) (term_of x);
    11.9  
   11.10  fun is_eqx x eq = case term_of eq of
   11.11     Const(@{const_name HOL.eq},_)$l$r => l aconv term_of x orelse r aconv term_of x
    12.1 --- a/src/HOL/Decision_Procs/mir_tac.ML	Wed Aug 10 18:02:16 2011 -0700
    12.2 +++ b/src/HOL/Decision_Procs/mir_tac.ML	Wed Aug 10 18:07:32 2011 -0700
    12.3 @@ -76,7 +76,7 @@
    12.4      val (fm',np) = List.foldr (fn ((x, T), (fm,n)) => mk_all ((x, T), (fm,n)))
    12.5        (List.foldr HOLogic.mk_imp c rhs, np) ps
    12.6      val (vs, _) = List.partition (fn t => q orelse (type_of t) = nT)
    12.7 -      (OldTerm.term_frees fm' @ OldTerm.term_vars fm');
    12.8 +      (Misc_Legacy.term_frees fm' @ Misc_Legacy.term_vars fm');
    12.9      val fm2 = List.foldr mk_all2 fm' vs
   12.10    in (fm2, np + length vs, length rhs) end;
   12.11  
    13.1 --- a/src/HOL/HOL.thy	Wed Aug 10 18:02:16 2011 -0700
    13.2 +++ b/src/HOL/HOL.thy	Wed Aug 10 18:07:32 2011 -0700
    13.3 @@ -15,7 +15,6 @@
    13.4    "~~/src/Tools/intuitionistic.ML"
    13.5    "~~/src/Tools/project_rule.ML"
    13.6    "~~/src/Tools/cong_tac.ML"
    13.7 -  "~~/src/Tools/misc_legacy.ML"
    13.8    "~~/src/Provers/hypsubst.ML"
    13.9    "~~/src/Provers/splitter.ML"
   13.10    "~~/src/Provers/classical.ML"
    14.1 --- a/src/HOL/Import/proof_kernel.ML	Wed Aug 10 18:02:16 2011 -0700
    14.2 +++ b/src/HOL/Import/proof_kernel.ML	Wed Aug 10 18:07:32 2011 -0700
    14.3 @@ -1059,7 +1059,7 @@
    14.4        val ct = cprop_of thm
    14.5        val t = term_of ct
    14.6        val thy = theory_of_cterm ct
    14.7 -      val frees = OldTerm.term_frees t
    14.8 +      val frees = Misc_Legacy.term_frees t
    14.9        val freenames = Term.add_free_names t []
   14.10        val is_old_name = member (op =) freenames
   14.11        fun name_of (Free (n, _)) = n
   14.12 @@ -1339,9 +1339,9 @@
   14.13      let
   14.14          val _ = message "INST_TYPE:"
   14.15          val _ = if_debug pth hth
   14.16 -        val tys_before = OldTerm.add_term_tfrees (prop_of th,[])
   14.17 +        val tys_before = Misc_Legacy.add_term_tfrees (prop_of th,[])
   14.18          val th1 = Thm.varifyT_global th
   14.19 -        val tys_after = OldTerm.add_term_tvars (prop_of th1,[])
   14.20 +        val tys_after = Misc_Legacy.add_term_tvars (prop_of th1,[])
   14.21          val tyinst = map (fn (bef, iS) =>
   14.22                               (case try (Lib.assoc (TFree bef)) lambda of
   14.23                                    SOME ty => (ctyp_of thy (TVar iS), ctyp_of thy ty)
   14.24 @@ -2002,7 +2002,7 @@
   14.25              val c = case concl_of th2 of
   14.26                          _ $ (Const(@{const_name Ex},_) $ Abs(_,_,Const(@{const_name Set.member},_) $ _ $ c)) => c
   14.27                        | _ => raise ERR "new_type_definition" "Bad type definition theorem"
   14.28 -            val tfrees = OldTerm.term_tfrees c
   14.29 +            val tfrees = Misc_Legacy.term_tfrees c
   14.30              val tnames = map fst tfrees
   14.31              val tsyn = mk_syn thy tycname
   14.32              val typ = (tycname,tnames,tsyn)
   14.33 @@ -2075,7 +2075,7 @@
   14.34              val c = case concl_of th2 of
   14.35                          _ $ (Const(@{const_name Ex},_) $ Abs(_,_,Const(@{const_name Set.member},_) $ _ $ c)) => c
   14.36                        | _ => raise ERR "type_introduction" "Bad type definition theorem"
   14.37 -            val tfrees = OldTerm.term_tfrees c
   14.38 +            val tfrees = Misc_Legacy.term_tfrees c
   14.39              val tnames = sort_strings (map fst tfrees)
   14.40              val tsyn = mk_syn thy tycname
   14.41              val typ = (tycname,tnames,tsyn)
    15.1 --- a/src/HOL/Import/shuffler.ML	Wed Aug 10 18:02:16 2011 -0700
    15.2 +++ b/src/HOL/Import/shuffler.ML	Wed Aug 10 18:07:32 2011 -0700
    15.3 @@ -223,8 +223,8 @@
    15.4  
    15.5  fun freeze_thaw_term t =
    15.6      let
    15.7 -        val tvars = OldTerm.term_tvars t
    15.8 -        val tfree_names = OldTerm.add_term_tfree_names(t,[])
    15.9 +        val tvars = Misc_Legacy.term_tvars t
   15.10 +        val tfree_names = Misc_Legacy.add_term_tfree_names(t,[])
   15.11          val (type_inst,_) =
   15.12              fold (fn (w as (v,_), S) => fn (inst, used) =>
   15.13                        let
   15.14 @@ -243,7 +243,7 @@
   15.15    | inst_tfrees thy ((name,U)::rest) thm =
   15.16      let
   15.17          val cU = ctyp_of thy U
   15.18 -        val tfrees = OldTerm.add_term_tfrees (prop_of thm,[])
   15.19 +        val tfrees = Misc_Legacy.add_term_tfrees (prop_of thm,[])
   15.20          val (rens, thm') = Thm.varifyT_global'
   15.21      (remove (op = o apsnd fst) name tfrees) thm
   15.22          val mid =
   15.23 @@ -494,7 +494,7 @@
   15.24      let
   15.25          val thy = Thm.theory_of_thm th
   15.26          val c = prop_of th
   15.27 -        val vars = OldTerm.add_term_frees (c, OldTerm.add_term_vars(c,[]))
   15.28 +        val vars = Misc_Legacy.add_term_frees (c, Misc_Legacy.add_term_vars(c,[]))
   15.29      in
   15.30          Drule.forall_intr_list (map (cterm_of thy) vars) th
   15.31      end
   15.32 @@ -560,7 +560,7 @@
   15.33  
   15.34  fun set_prop thy t =
   15.35      let
   15.36 -        val vars = OldTerm.add_term_frees (t, OldTerm.add_term_vars (t,[]))
   15.37 +        val vars = Misc_Legacy.add_term_frees (t, Misc_Legacy.add_term_vars (t,[]))
   15.38          val closed_t = fold_rev Logic.all vars t
   15.39          val rew_th = norm_term thy closed_t
   15.40          val rhs = Thm.rhs_of rew_th
    16.1 --- a/src/HOL/IsaMakefile	Wed Aug 10 18:02:16 2011 -0700
    16.2 +++ b/src/HOL/IsaMakefile	Wed Aug 10 18:07:32 2011 -0700
    16.3 @@ -122,7 +122,6 @@
    16.4    $(SRC)/Provers/hypsubst.ML \
    16.5    $(SRC)/Provers/quantifier1.ML \
    16.6    $(SRC)/Provers/splitter.ML \
    16.7 -  $(SRC)/Tools/cache_io.ML \
    16.8    $(SRC)/Tools/Code/code_haskell.ML \
    16.9    $(SRC)/Tools/Code/code_ml.ML \
   16.10    $(SRC)/Tools/Code/code_namespace.ML \
   16.11 @@ -139,7 +138,9 @@
   16.12    $(SRC)/Tools/IsaPlanner/rw_tools.ML \
   16.13    $(SRC)/Tools/IsaPlanner/zipper.ML \
   16.14    $(SRC)/Tools/atomize_elim.ML \
   16.15 +  $(SRC)/Tools/cache_io.ML \
   16.16    $(SRC)/Tools/case_product.ML \
   16.17 +  $(SRC)/Tools/codegen.ML \
   16.18    $(SRC)/Tools/coherent.ML \
   16.19    $(SRC)/Tools/cong_tac.ML \
   16.20    $(SRC)/Tools/eqsubst.ML \
    17.1 --- a/src/HOL/Matrix/Compute_Oracle/linker.ML	Wed Aug 10 18:02:16 2011 -0700
    17.2 +++ b/src/HOL/Matrix/Compute_Oracle/linker.ML	Wed Aug 10 18:07:32 2011 -0700
    17.3 @@ -90,7 +90,7 @@
    17.4      let
    17.5          val cs = distinct_constants (filter is_polymorphic cs)
    17.6          val old_cs = cs
    17.7 -(*      fun collect_tvars ty tab = fold (fn v => fn tab => Typtab.update (TVar v, ()) tab) (OldTerm.typ_tvars ty) tab
    17.8 +(*      fun collect_tvars ty tab = fold (fn v => fn tab => Typtab.update (TVar v, ()) tab) (Misc_Legacy.typ_tvars ty) tab
    17.9          val tvars_count = length (Typtab.keys (fold (fn c => fn tab => collect_tvars (typ_of_constant c) tab) cs Typtab.empty))
   17.10          fun tvars_of ty = collect_tvars ty Typtab.empty
   17.11          val cs = map (fn c => (c, tvars_of (typ_of_constant c))) cs
   17.12 @@ -259,10 +259,10 @@
   17.13  let
   17.14      val (left, right) = collect_consts_of_thm th
   17.15      val polycs = filter Linker.is_polymorphic left
   17.16 -    val tytab = fold (fn p => fn tab => fold (fn n => fn tab => Typtab.update (TVar n, ()) tab) (OldTerm.typ_tvars (Linker.typ_of_constant p)) tab) polycs Typtab.empty
   17.17 +    val tytab = fold (fn p => fn tab => fold (fn n => fn tab => Typtab.update (TVar n, ()) tab) (Misc_Legacy.typ_tvars (Linker.typ_of_constant p)) tab) polycs Typtab.empty
   17.18      fun check_const (c::cs) cs' =
   17.19          let
   17.20 -            val tvars = OldTerm.typ_tvars (Linker.typ_of_constant c)
   17.21 +            val tvars = Misc_Legacy.typ_tvars (Linker.typ_of_constant c)
   17.22              val wrong = fold (fn n => fn wrong => wrong orelse is_none (Typtab.lookup tytab (TVar n))) tvars false
   17.23          in
   17.24              if wrong then raise PCompute "right hand side of theorem contains type variables which do not occur on the left hand side"
    18.1 --- a/src/HOL/Matrix/matrixlp.ML	Wed Aug 10 18:02:16 2011 -0700
    18.2 +++ b/src/HOL/Matrix/matrixlp.ML	Wed Aug 10 18:07:32 2011 -0700
    18.3 @@ -19,7 +19,7 @@
    18.4  fun inst_real thm =
    18.5    let val certT = ctyp_of (Thm.theory_of_thm thm) in
    18.6      Drule.export_without_context (Thm.instantiate
    18.7 -      ([(certT (TVar (hd (OldTerm.term_tvars (prop_of thm)))), certT HOLogic.realT)], []) thm)
    18.8 +      ([(certT (TVar (hd (Misc_Legacy.term_tvars (prop_of thm)))), certT HOLogic.realT)], []) thm)
    18.9    end
   18.10  
   18.11  local
   18.12 @@ -57,7 +57,7 @@
   18.13      let
   18.14          val certT = Thm.ctyp_of (Thm.theory_of_thm thm);
   18.15          val ord = prod_ord (prod_ord string_ord int_ord) (list_ord string_ord)
   18.16 -        val v = TVar (hd (sort ord (OldTerm.term_tvars (prop_of thm))))
   18.17 +        val v = TVar (hd (sort ord (Misc_Legacy.term_tvars (prop_of thm))))
   18.18      in
   18.19          Drule.export_without_context (Thm.instantiate ([(certT v, certT ty)], []) thm)
   18.20      end
    19.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Wed Aug 10 18:02:16 2011 -0700
    19.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Wed Aug 10 18:07:32 2011 -0700
    19.3 @@ -1414,7 +1414,7 @@
    19.4  
    19.5      val _ = warning "defining recursion combinator ...";
    19.6  
    19.7 -    val used = List.foldr OldTerm.add_typ_tfree_names [] recTs;
    19.8 +    val used = List.foldr Misc_Legacy.add_typ_tfree_names [] recTs;
    19.9  
   19.10      val (rec_result_Ts', rec_fn_Ts') = Datatype_Prop.make_primrec_Ts descr' sorts used;
   19.11  
    20.1 --- a/src/HOL/Nominal/nominal_fresh_fun.ML	Wed Aug 10 18:02:16 2011 -0700
    20.2 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Wed Aug 10 18:07:32 2011 -0700
    20.3 @@ -69,7 +69,7 @@
    20.4     val bvs = map_index (Bound o fst) ps;
    20.5  (* select variables of the right class *)
    20.6     val vs = filter (fn t => is_of_fs_name (fastype_of1 (Ts, t)))
    20.7 -     (OldTerm.term_frees goal @ bvs);
    20.8 +     (Misc_Legacy.term_frees goal @ bvs);
    20.9  (* build the tuple *)
   20.10     val s = (Library.foldr1 (fn (v, s) =>
   20.11         HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s) vs)
   20.12 @@ -78,7 +78,7 @@
   20.13     val at_name_inst_thm = get_dyn_thm thy ("at_"^atom_basename^"_inst") atom_basename;
   20.14     val exists_fresh' = at_name_inst_thm RS at_exists_fresh';
   20.15  (* find the variable we want to instantiate *)
   20.16 -   val x = hd (OldTerm.term_vars (prop_of exists_fresh'));
   20.17 +   val x = hd (Misc_Legacy.term_vars (prop_of exists_fresh'));
   20.18   in
   20.19     (cut_inst_tac_term' [(x,s)] exists_fresh' 1 THEN
   20.20     rtac fs_name_thm 1 THEN
   20.21 @@ -137,7 +137,7 @@
   20.22      val fresh_perm_app = Global_Theory.get_thms thy "fresh_perm_app";
   20.23      val ss' = ss addsimps fresh_prod::abs_fresh;
   20.24      val ss'' = ss' addsimps fresh_perm_app;
   20.25 -    val x = hd (tl (OldTerm.term_vars (prop_of exI)));
   20.26 +    val x = hd (tl (Misc_Legacy.term_vars (prop_of exI)));
   20.27      val goal = nth (prems_of thm) (i-1);
   20.28      val atom_name_opt = get_inner_fresh_fun goal;
   20.29      val n = length (Logic.strip_params goal);
   20.30 @@ -152,7 +152,7 @@
   20.31      val pt_name_inst = get_dyn_thm thy ("pt_"^atom_basename^"_inst") atom_basename;
   20.32      val at_name_inst = get_dyn_thm thy ("at_"^atom_basename^"_inst") atom_basename;
   20.33      fun inst_fresh vars params i st =
   20.34 -   let val vars' = OldTerm.term_vars (prop_of st);
   20.35 +   let val vars' = Misc_Legacy.term_vars (prop_of st);
   20.36         val thy = theory_of_thm st;
   20.37     in case subtract (op =) vars vars' of
   20.38       [x] => Seq.single (Thm.instantiate ([],[(cterm_of thy x,cterm_of thy (list_abs (params,Bound 0)))]) st)
   20.39 @@ -161,7 +161,7 @@
   20.40    in
   20.41    ((fn st =>
   20.42    let
   20.43 -    val vars = OldTerm.term_vars (prop_of st);
   20.44 +    val vars = Misc_Legacy.term_vars (prop_of st);
   20.45      val params = Logic.strip_params (nth (prems_of st) (i-1))
   20.46      (* The tactics which solve the subgoals generated
   20.47         by the conditionnal rewrite rule. *)
    21.1 --- a/src/HOL/Nominal/nominal_primrec.ML	Wed Aug 10 18:02:16 2011 -0700
    21.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Wed Aug 10 18:07:32 2011 -0700
    21.3 @@ -76,7 +76,7 @@
    21.4      else
    21.5       (check_vars "repeated variable names in pattern: " (duplicates (op =) lfrees);
    21.6        check_vars "extra variables on rhs: "
    21.7 -        (map dest_Free (OldTerm.term_frees rhs) |> subtract (op =) lfrees
    21.8 +        (map dest_Free (Misc_Legacy.term_frees rhs) |> subtract (op =) lfrees
    21.9            |> filter_out (is_fixed o fst));
   21.10        case AList.lookup (op =) rec_fns fname of
   21.11          NONE =>
    22.1 --- a/src/HOL/Statespace/state_space.ML	Wed Aug 10 18:02:16 2011 -0700
    22.2 +++ b/src/HOL/Statespace/state_space.ML	Wed Aug 10 18:07:32 2011 -0700
    22.3 @@ -472,7 +472,7 @@
    22.4    let
    22.5      val ctxt' = fold (Variable.declare_typ o TFree) env ctxt;
    22.6      val T = Syntax.read_typ ctxt' raw_T;
    22.7 -    val env' = OldTerm.add_typ_tfrees (T, env);
    22.8 +    val env' = Misc_Legacy.add_typ_tfrees (T, env);
    22.9    in (T, env') end;
   22.10  
   22.11  fun cert_typ ctxt raw_T env =
   22.12 @@ -480,7 +480,7 @@
   22.13      val thy = Proof_Context.theory_of ctxt;
   22.14      val T = Type.no_tvars (Sign.certify_typ thy raw_T)
   22.15        handle TYPE (msg, _, _) => error msg;
   22.16 -    val env' = OldTerm.add_typ_tfrees (T, env);
   22.17 +    val env' = Misc_Legacy.add_typ_tfrees (T, env);
   22.18    in (T, env') end;
   22.19  
   22.20  fun gen_define_statespace prep_typ state_space args name parents comps thy =
    23.1 --- a/src/HOL/Tools/ATP/atp_reconstruct.ML	Wed Aug 10 18:02:16 2011 -0700
    23.2 +++ b/src/HOL/Tools/ATP/atp_reconstruct.ML	Wed Aug 10 18:07:32 2011 -0700
    23.3 @@ -545,12 +545,12 @@
    23.4          |> HOLogic.dest_eq
    23.5      in
    23.6        (Definition (name, t1, t2),
    23.7 -       fold Variable.declare_term (maps OldTerm.term_frees [t1, t2]) ctxt)
    23.8 +       fold Variable.declare_term (maps Misc_Legacy.term_frees [t1, t2]) ctxt)
    23.9      end
   23.10    | decode_line sym_tab (Inference (name, u, deps)) ctxt =
   23.11      let val t = u |> uncombined_etc_prop_from_atp ctxt true sym_tab in
   23.12        (Inference (name, t, deps),
   23.13 -       fold Variable.declare_term (OldTerm.term_frees t) ctxt)
   23.14 +       fold Variable.declare_term (Misc_Legacy.term_frees t) ctxt)
   23.15      end
   23.16  fun decode_lines ctxt sym_tab lines =
   23.17    fst (fold_map (decode_line sym_tab) lines ctxt)
    24.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Wed Aug 10 18:02:16 2011 -0700
    24.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Wed Aug 10 18:07:32 2011 -0700
    24.3 @@ -1457,8 +1457,8 @@
    24.4    #> List.foldl add_classes Symtab.empty
    24.5    #> delete_type #> Symtab.keys
    24.6  
    24.7 -val tfree_classes_of_terms = classes_of_terms OldTerm.term_tfrees
    24.8 -val tvar_classes_of_terms = classes_of_terms OldTerm.term_tvars
    24.9 +val tfree_classes_of_terms = classes_of_terms Misc_Legacy.term_tfrees
   24.10 +val tvar_classes_of_terms = classes_of_terms Misc_Legacy.term_tvars
   24.11  
   24.12  fun fold_type_constrs f (Type (s, Ts)) x =
   24.13      fold (fold_type_constrs f) Ts (f (s, x))
    25.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Wed Aug 10 18:02:16 2011 -0700
    25.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Wed Aug 10 18:07:32 2011 -0700
    25.3 @@ -77,7 +77,7 @@
    25.4        else Balanced_Tree.make (fn (T, U) => Type (@{type_name Sum_Type.sum}, [T, U])) branchTs;
    25.5      val arities = remove (op =) 0 (Datatype_Aux.get_arities descr');
    25.6      val unneeded_vars =
    25.7 -      subtract (op =) (List.foldr OldTerm.add_typ_tfree_names [] (leafTs' @ branchTs)) (hd tyvars);
    25.8 +      subtract (op =) (List.foldr Misc_Legacy.add_typ_tfree_names [] (leafTs' @ branchTs)) (hd tyvars);
    25.9      val leafTs = leafTs' @ map (fn n => TFree (n, (the o AList.lookup (op =) sorts) n)) unneeded_vars;
   25.10      val recTs = Datatype_Aux.get_rec_types descr' sorts;
   25.11      val (newTs, oldTs) = chop (length (hd descr)) recTs;
   25.12 @@ -372,7 +372,7 @@
   25.13          val prop = Thm.prop_of thm;
   25.14          val _ $ (_ $ ((S as Const (_, Type (_, [U, _]))) $ _ )) $
   25.15            (_ $ (_ $ (r $ (a $ _)) $ _)) = Type.legacy_freeze prop;
   25.16 -        val used = OldTerm.add_term_tfree_names (a, []);
   25.17 +        val used = Misc_Legacy.add_term_tfree_names (a, []);
   25.18  
   25.19          fun mk_thm i =
   25.20            let
   25.21 @@ -676,7 +676,7 @@
   25.22            let
   25.23              val (cargs', sorts'') = fold_map (prep_typ tmp_thy) cargs sorts';
   25.24              val _ =
   25.25 -              (case subtract (op =) tvs (fold (curry OldTerm.add_typ_tfree_names) cargs' []) of
   25.26 +              (case subtract (op =) tvs (fold (curry Misc_Legacy.add_typ_tfree_names) cargs' []) of
   25.27                  [] => ()
   25.28                | vs => error ("Extra type variables on rhs: " ^ commas vs));
   25.29              val c = Sign.full_name_path tmp_thy tname' cname;
    26.1 --- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Wed Aug 10 18:02:16 2011 -0700
    26.2 +++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Wed Aug 10 18:07:32 2011 -0700
    26.3 @@ -91,7 +91,7 @@
    26.4  
    26.5      val descr' = flat descr;
    26.6      val recTs = Datatype_Aux.get_rec_types descr' sorts;
    26.7 -    val used = List.foldr OldTerm.add_typ_tfree_names [] recTs;
    26.8 +    val used = List.foldr Misc_Legacy.add_typ_tfree_names [] recTs;
    26.9      val newTs = take (length (hd descr)) recTs;
   26.10  
   26.11      val induct_Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct)));
   26.12 @@ -279,7 +279,7 @@
   26.13  
   26.14      val descr' = flat descr;
   26.15      val recTs = Datatype_Aux.get_rec_types descr' sorts;
   26.16 -    val used = List.foldr OldTerm.add_typ_tfree_names [] recTs;
   26.17 +    val used = List.foldr Misc_Legacy.add_typ_tfree_names [] recTs;
   26.18      val newTs = take (length (hd descr)) recTs;
   26.19      val T' = TFree (singleton (Name.variant_list used) "'t", HOLogic.typeS);
   26.20  
    27.1 --- a/src/HOL/Tools/Datatype/datatype_aux.ML	Wed Aug 10 18:02:16 2011 -0700
    27.2 +++ b/src/HOL/Tools/Datatype/datatype_aux.ML	Wed Aug 10 18:07:32 2011 -0700
    27.3 @@ -144,7 +144,7 @@
    27.4      fun abstr (t1, t2) =
    27.5        (case t1 of
    27.6          NONE =>
    27.7 -          (case flt (OldTerm.term_frees t2) of
    27.8 +          (case flt (Misc_Legacy.term_frees t2) of
    27.9              [Free (s, T)] => SOME (absfree (s, T, t2))
   27.10            | _ => NONE)
   27.11        | SOME (_ $ t') => SOME (Abs ("x", fastype_of t', abstract_over (t', t2))))
    28.1 --- a/src/HOL/Tools/Datatype/datatype_case.ML	Wed Aug 10 18:02:16 2011 -0700
    28.2 +++ b/src/HOL/Tools/Datatype/datatype_case.ML	Wed Aug 10 18:07:32 2011 -0700
    28.3 @@ -318,7 +318,7 @@
    28.4              val _ = if length zs < i then raise CASE_ERROR ("", 0) else ();
    28.5              val (xs, ys) = chop i zs;
    28.6              val u = list_abs (ys, strip_abs_body t);
    28.7 -            val xs' = map Free (Name.variant_list (OldTerm.add_term_names (u, used))
    28.8 +            val xs' = map Free (Name.variant_list (Misc_Legacy.add_term_names (u, used))
    28.9                (map fst xs) ~~ map snd xs)
   28.10            in (xs', subst_bounds (rev xs', u)) end;
   28.11          fun is_dependent i t =
   28.12 @@ -379,9 +379,9 @@
   28.13  fun strip_case'' dest (pat, rhs) =
   28.14    (case dest (Term.add_free_names pat []) rhs of
   28.15      SOME (exp as Free _, clauses) =>
   28.16 -      if member op aconv (OldTerm.term_frees pat) exp andalso
   28.17 +      if member op aconv (Misc_Legacy.term_frees pat) exp andalso
   28.18          not (exists (fn (_, rhs') =>
   28.19 -          member op aconv (OldTerm.term_frees rhs') exp) clauses)
   28.20 +          member op aconv (Misc_Legacy.term_frees rhs') exp) clauses)
   28.21        then
   28.22          maps (strip_case'' dest) (map (fn (pat', rhs') =>
   28.23            (subst_free [(exp, pat')] pat, rhs')) clauses)
    29.1 --- a/src/HOL/Tools/Datatype/datatype_codegen.ML	Wed Aug 10 18:02:16 2011 -0700
    29.2 +++ b/src/HOL/Tools/Datatype/datatype_codegen.ML	Wed Aug 10 18:07:32 2011 -0700
    29.3 @@ -331,8 +331,8 @@
    29.4        let
    29.5          val ts1 = take i ts;
    29.6          val t :: ts2 = drop i ts;
    29.7 -        val names = List.foldr OldTerm.add_term_names
    29.8 -          (map (fst o fst o dest_Var) (List.foldr OldTerm.add_term_vars [] ts1)) ts1;
    29.9 +        val names = List.foldr Misc_Legacy.add_term_names
   29.10 +          (map (fst o fst o dest_Var) (List.foldr Misc_Legacy.add_term_vars [] ts1)) ts1;
   29.11          val (Ts, dT) = split_last (take (i+1) (binder_types T));
   29.12  
   29.13          fun pcase [] [] [] gr = ([], gr)
    30.1 --- a/src/HOL/Tools/Datatype/datatype_data.ML	Wed Aug 10 18:02:16 2011 -0700
    30.2 +++ b/src/HOL/Tools/Datatype/datatype_data.ML	Wed Aug 10 18:07:32 2011 -0700
    30.3 @@ -398,7 +398,7 @@
    30.4          Syntax.string_of_typ ctxt T);
    30.5      fun type_of_constr (cT as (_, T)) =
    30.6        let
    30.7 -        val frees = OldTerm.typ_tfrees T;
    30.8 +        val frees = Misc_Legacy.typ_tfrees T;
    30.9          val (tyco, vs) = (apsnd o map) dest_TFree (dest_Type (body_type T))
   30.10            handle TYPE _ => no_constr cT
   30.11          val _ = if has_duplicates (eq_fst (op =)) vs then no_constr cT else ();
    31.1 --- a/src/HOL/Tools/Datatype/datatype_prop.ML	Wed Aug 10 18:02:16 2011 -0700
    31.2 +++ b/src/HOL/Tools/Datatype/datatype_prop.ML	Wed Aug 10 18:07:32 2011 -0700
    31.3 @@ -210,7 +210,7 @@
    31.4    let
    31.5      val descr' = flat descr;
    31.6      val recTs = Datatype_Aux.get_rec_types descr' sorts;
    31.7 -    val used = List.foldr OldTerm.add_typ_tfree_names [] recTs;
    31.8 +    val used = List.foldr Misc_Legacy.add_typ_tfree_names [] recTs;
    31.9  
   31.10      val (rec_result_Ts, reccomb_fn_Ts) = make_primrec_Ts descr sorts used;
   31.11  
   31.12 @@ -261,7 +261,7 @@
   31.13    let
   31.14      val descr' = flat descr;
   31.15      val recTs = Datatype_Aux.get_rec_types descr' sorts;
   31.16 -    val used = List.foldr OldTerm.add_typ_tfree_names [] recTs;
   31.17 +    val used = List.foldr Misc_Legacy.add_typ_tfree_names [] recTs;
   31.18      val newTs = take (length (hd descr)) recTs;
   31.19      val T' = TFree (singleton (Name.variant_list used) "'t", HOLogic.typeS);
   31.20  
   31.21 @@ -308,7 +308,7 @@
   31.22    let
   31.23      val descr' = flat descr;
   31.24      val recTs = Datatype_Aux.get_rec_types descr' sorts;
   31.25 -    val used' = List.foldr OldTerm.add_typ_tfree_names [] recTs;
   31.26 +    val used' = List.foldr Misc_Legacy.add_typ_tfree_names [] recTs;
   31.27      val newTs = take (length (hd descr)) recTs;
   31.28      val T' = TFree (singleton (Name.variant_list used') "'t", HOLogic.typeS);
   31.29      val P = Free ("P", T' --> HOLogic.boolT);
    32.1 --- a/src/HOL/Tools/Meson/meson_clausify.ML	Wed Aug 10 18:02:16 2011 -0700
    32.2 +++ b/src/HOL/Tools/Meson/meson_clausify.ML	Wed Aug 10 18:07:32 2011 -0700
    32.3 @@ -65,7 +65,7 @@
    32.4      fun dec_sko (Const (@{const_name Ex}, _) $ (body as Abs (_, T, p))) rhss =
    32.5          (*Existential: declare a Skolem function, then insert into body and continue*)
    32.6          let
    32.7 -          val args = OldTerm.term_frees body
    32.8 +          val args = Misc_Legacy.term_frees body
    32.9            (* Forms a lambda-abstraction over the formal parameters *)
   32.10            val rhs =
   32.11              list_abs_free (map dest_Free args,
   32.12 @@ -75,7 +75,7 @@
   32.13          in dec_sko (subst_bound (comb, p)) (rhs :: rhss) end
   32.14        | dec_sko (Const (@{const_name All},_) $ Abs (a, T, p)) rhss =
   32.15          (*Universal quant: insert a free variable into body and continue*)
   32.16 -        let val fname = singleton (Name.variant_list (OldTerm.add_term_names (p, []))) a
   32.17 +        let val fname = singleton (Name.variant_list (Misc_Legacy.add_term_names (p, []))) a
   32.18          in dec_sko (subst_bound (Free(fname,T), p)) rhss end
   32.19        | dec_sko (@{const conj} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
   32.20        | dec_sko (@{const disj} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
   32.21 @@ -92,9 +92,9 @@
   32.22    | is_quasi_lambda_free (Abs _) = false
   32.23    | is_quasi_lambda_free _ = true
   32.24  
   32.25 -val [f_B,g_B] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_B}));
   32.26 -val [g_C,f_C] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_C}));
   32.27 -val [f_S,g_S] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_S}));
   32.28 +val [f_B,g_B] = map (cterm_of @{theory}) (Misc_Legacy.term_vars (prop_of @{thm abs_B}));
   32.29 +val [g_C,f_C] = map (cterm_of @{theory}) (Misc_Legacy.term_vars (prop_of @{thm abs_C}));
   32.30 +val [f_S,g_S] = map (cterm_of @{theory}) (Misc_Legacy.term_vars (prop_of @{thm abs_S}));
   32.31  
   32.32  (* FIXME: Requires more use of cterm constructors. *)
   32.33  fun abstract ct =
    33.1 --- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Wed Aug 10 18:02:16 2011 -0700
    33.2 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Wed Aug 10 18:07:32 2011 -0700
    33.3 @@ -372,7 +372,7 @@
    33.4        val subst' = Thm.incr_indexes (imax+1) (if pos then subst_em else ssubst_em)
    33.5        val _ = trace_msg ctxt (fn () => "subst' " ^ Display.string_of_thm ctxt subst')
    33.6        val eq_terms = map (pairself (cterm_of thy))
    33.7 -        (ListPair.zip (OldTerm.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm]))
    33.8 +        (ListPair.zip (Misc_Legacy.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm]))
    33.9    in  cterm_instantiate eq_terms subst'  end;
   33.10  
   33.11  val factor = Seq.hd o distinct_subgoals_tac
    34.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Wed Aug 10 18:02:16 2011 -0700
    34.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Wed Aug 10 18:07:32 2011 -0700
    34.3 @@ -560,7 +560,7 @@
    34.4  
    34.5  fun conv ctxt p =
    34.6    Qelim.gen_qelim_conv (Simplifier.rewrite conv_ss) (Simplifier.rewrite presburger_ss) (Simplifier.rewrite conv_ss)
    34.7 -    (cons o term_of) (OldTerm.term_frees (term_of p)) (linearize_conv ctxt) (integer_nnf_conv ctxt)
    34.8 +    (cons o term_of) (Misc_Legacy.term_frees (term_of p)) (linearize_conv ctxt) (integer_nnf_conv ctxt)
    34.9      (cooperex_conv ctxt) p
   34.10    handle CTERM s => raise COOPER "bad cterm"
   34.11         | THM s => raise COOPER "bad thm"
   34.12 @@ -759,8 +759,8 @@
   34.13  in 
   34.14  fun is_relevant ctxt ct = 
   34.15   subset (op aconv) (term_constants (term_of ct) , snd (get ctxt))
   34.16 - andalso forall (fn Free (_,T) => member (op =) [@{typ int}, @{typ nat}] T) (OldTerm.term_frees (term_of ct))
   34.17 - andalso forall (fn Var (_,T) => member (op =) [@{typ int}, @{typ nat}] T) (OldTerm.term_vars (term_of ct));
   34.18 + andalso forall (fn Free (_,T) => member (op =) [@{typ int}, @{typ nat}] T) (Misc_Legacy.term_frees (term_of ct))
   34.19 + andalso forall (fn Var (_,T) => member (op =) [@{typ int}, @{typ nat}] T) (Misc_Legacy.term_vars (term_of ct));
   34.20  
   34.21  fun int_nat_terms ctxt ct =
   34.22   let 
    35.1 --- a/src/HOL/Tools/Sledgehammer/async_manager.ML	Wed Aug 10 18:02:16 2011 -0700
    35.2 +++ b/src/HOL/Tools/Sledgehammer/async_manager.ML	Wed Aug 10 18:07:32 2011 -0700
    35.3 @@ -144,7 +144,7 @@
    35.4                NONE
    35.5              else
    35.6                let
    35.7 -                val _ = List.app (Simple_Thread.interrupt o #1) canceling
    35.8 +                val _ = List.app (Simple_Thread.interrupt_unsynchronized o #1) canceling
    35.9                  val canceling' = filter (Thread.isActive o #1) canceling
   35.10                  val state' = make_state manager timeout_heap' active canceling' messages store;
   35.11                in SOME (map #2 timeout_threads, state') end
    36.1 --- a/src/HOL/Tools/TFL/casesplit.ML	Wed Aug 10 18:02:16 2011 -0700
    36.2 +++ b/src/HOL/Tools/TFL/casesplit.ML	Wed Aug 10 18:07:32 2011 -0700
    36.3 @@ -56,9 +56,9 @@
    36.4        val abs_ct = ctermify abst;
    36.5        val free_ct = ctermify x;
    36.6  
    36.7 -      val casethm_vars = rev (OldTerm.term_vars (Thm.concl_of case_thm));
    36.8 +      val casethm_vars = rev (Misc_Legacy.term_vars (Thm.concl_of case_thm));
    36.9  
   36.10 -      val casethm_tvars = OldTerm.term_tvars (Thm.concl_of case_thm);
   36.11 +      val casethm_tvars = Misc_Legacy.term_tvars (Thm.concl_of case_thm);
   36.12        val (Pv, Dv, type_insts) =
   36.13            case (Thm.concl_of case_thm) of
   36.14              (_ $ ((Pv as Var(P,Pty)) $ (Dv as Var(D, Dty)))) =>
    37.1 --- a/src/HOL/Tools/TFL/rules.ML	Wed Aug 10 18:02:16 2011 -0700
    37.2 +++ b/src/HOL/Tools/TFL/rules.ML	Wed Aug 10 18:07:32 2011 -0700
    37.3 @@ -160,7 +160,7 @@
    37.4   *---------------------------------------------------------------------------*)
    37.5  local val thy = Thm.theory_of_thm disjI1
    37.6        val prop = Thm.prop_of disjI1
    37.7 -      val [P,Q] = OldTerm.term_vars prop
    37.8 +      val [P,Q] = Misc_Legacy.term_vars prop
    37.9        val disj1 = Thm.forall_intr (Thm.cterm_of thy Q) disjI1
   37.10  in
   37.11  fun DISJ1 thm tm = thm RS (Thm.forall_elim (Dcterm.drop_prop tm) disj1)
   37.12 @@ -169,7 +169,7 @@
   37.13  
   37.14  local val thy = Thm.theory_of_thm disjI2
   37.15        val prop = Thm.prop_of disjI2
   37.16 -      val [P,Q] = OldTerm.term_vars prop
   37.17 +      val [P,Q] = Misc_Legacy.term_vars prop
   37.18        val disj2 = Thm.forall_intr (Thm.cterm_of thy P) disjI2
   37.19  in
   37.20  fun DISJ2 tm thm = thm RS (Thm.forall_elim (Dcterm.drop_prop tm) disj2)
   37.21 @@ -263,7 +263,7 @@
   37.22  local (* this is fragile *)
   37.23        val thy = Thm.theory_of_thm spec
   37.24        val prop = Thm.prop_of spec
   37.25 -      val x = hd (tl (OldTerm.term_vars prop))
   37.26 +      val x = hd (tl (Misc_Legacy.term_vars prop))
   37.27        val cTV = ctyp_of thy (type_of x)
   37.28        val gspec = Thm.forall_intr (cterm_of thy x) spec
   37.29  in
   37.30 @@ -280,7 +280,7 @@
   37.31  (* Not optimized! Too complicated. *)
   37.32  local val thy = Thm.theory_of_thm allI
   37.33        val prop = Thm.prop_of allI
   37.34 -      val [P] = OldTerm.add_term_vars (prop, [])
   37.35 +      val [P] = Misc_Legacy.add_term_vars (prop, [])
   37.36        fun cty_theta s = map (fn (i, (S, ty)) => (ctyp_of s (TVar (i, S)), ctyp_of s ty))
   37.37        fun ctm_theta s = map (fn (i, (_, tm2)) =>
   37.38                               let val ctm2 = cterm_of s tm2
   37.39 @@ -310,7 +310,7 @@
   37.40     let val thy = Thm.theory_of_thm thm
   37.41         val prop = Thm.prop_of thm
   37.42         val tycheck = cterm_of thy
   37.43 -       val vlist = map tycheck (OldTerm.add_term_vars (prop, []))
   37.44 +       val vlist = map tycheck (Misc_Legacy.add_term_vars (prop, []))
   37.45    in GENL vlist thm
   37.46    end;
   37.47  
   37.48 @@ -350,7 +350,7 @@
   37.49  
   37.50  local val thy = Thm.theory_of_thm exI
   37.51        val prop = Thm.prop_of exI
   37.52 -      val [P,x] = OldTerm.term_vars prop
   37.53 +      val [P,x] = Misc_Legacy.term_vars prop
   37.54  in
   37.55  fun EXISTS (template,witness) thm =
   37.56     let val thy = Thm.theory_of_thm thm
   37.57 @@ -501,7 +501,7 @@
   37.58                  val (f,args) = USyntax.strip_comb (get_lhs eq)
   37.59                  val (vstrl,_) = USyntax.strip_abs f
   37.60                  val names  =
   37.61 -                  Name.variant_list (OldTerm.add_term_names(body, [])) (map (#1 o dest_Free) vstrl)
   37.62 +                  Name.variant_list (Misc_Legacy.add_term_names(body, [])) (map (#1 o dest_Free) vstrl)
   37.63              in get (rst, n+1, (names,n)::L) end
   37.64              handle TERM _ => get (rst, n+1, L)
   37.65                | Utils.ERR _ => get (rst, n+1, L);
   37.66 @@ -742,7 +742,7 @@
   37.67                val thy = Thm.theory_of_thm thm
   37.68                val Const("==>",_) $ (Const(@{const_name Trueprop},_) $ A) $ _ = Thm.prop_of thm
   37.69                fun genl tm = let val vlist = subtract (op aconv) globals
   37.70 -                                           (OldTerm.add_term_frees(tm,[]))
   37.71 +                                           (Misc_Legacy.add_term_frees(tm,[]))
   37.72                              in fold_rev Forall vlist tm
   37.73                              end
   37.74                (*--------------------------------------------------------------
   37.75 @@ -780,7 +780,7 @@
   37.76      (if (is_cong thm) then cong_prover else restrict_prover) ss thm
   37.77      end
   37.78      val ctm = cprop_of th
   37.79 -    val names = OldTerm.add_term_names (term_of ctm, [])
   37.80 +    val names = Misc_Legacy.add_term_names (term_of ctm, [])
   37.81      val th1 = Raw_Simplifier.rewrite_cterm (false,true,false)
   37.82        (prover names) (ss0 addsimps [cut_lemma'] addeqcongs congs) ctm
   37.83      val th2 = Thm.equal_elim th1 th
    38.1 --- a/src/HOL/Tools/TFL/tfl.ML	Wed Aug 10 18:02:16 2011 -0700
    38.2 +++ b/src/HOL/Tools/TFL/tfl.ML	Wed Aug 10 18:07:32 2011 -0700
    38.3 @@ -322,7 +322,7 @@
    38.4       val dummy = map (no_repeat_vars thy) pats
    38.5       val rows = ListPair.zip (map (fn x => ([]:term list,[x])) pats,
    38.6                                map_index (fn (i, t) => (t,(i,true))) R)
    38.7 -     val names = List.foldr OldTerm.add_term_names [] R
    38.8 +     val names = List.foldr Misc_Legacy.add_term_names [] R
    38.9       val atype = type_of(hd pats)
   38.10       and aname = singleton (Name.variant_list names) "a"
   38.11       val a = Free(aname,atype)
   38.12 @@ -480,7 +480,7 @@
   38.13       val tych = Thry.typecheck thy
   38.14       val WFREC_THM0 = Rules.ISPEC (tych functional) Thms.WFREC_COROLLARY
   38.15       val Const(@{const_name All},_) $ Abs(Rname,Rtype,_) = concl WFREC_THM0
   38.16 -     val R = Free (singleton (Name.variant_list (List.foldr OldTerm.add_term_names [] eqns)) Rname,
   38.17 +     val R = Free (singleton (Name.variant_list (List.foldr Misc_Legacy.add_term_names [] eqns)) Rname,
   38.18                     Rtype)
   38.19       val WFREC_THM = Rules.ISPECL [tych R, tych g] WFREC_THM0
   38.20       val ([proto_def, WFR],_) = USyntax.strip_imp(concl WFREC_THM)
   38.21 @@ -677,7 +677,7 @@
   38.22   let val tych = Thry.typecheck thy
   38.23       val ty_info = Thry.induct_info thy
   38.24   in fn pats =>
   38.25 - let val names = List.foldr OldTerm.add_term_names [] pats
   38.26 + let val names = List.foldr Misc_Legacy.add_term_names [] pats
   38.27       val T = type_of (hd pats)
   38.28       val aname = singleton (Name.variant_list names) "a"
   38.29       val vname = singleton (Name.variant_list (aname::names)) "v"
   38.30 @@ -830,7 +830,7 @@
   38.31      val (pats,TCsl) = ListPair.unzip pat_TCs_list
   38.32      val case_thm = complete_cases thy pats
   38.33      val domain = (type_of o hd) pats
   38.34 -    val Pname = singleton (Name.variant_list (List.foldr (Library.foldr OldTerm.add_term_names)
   38.35 +    val Pname = singleton (Name.variant_list (List.foldr (Library.foldr Misc_Legacy.add_term_names)
   38.36                                [] (pats::TCsl))) "P"
   38.37      val P = Free(Pname, domain --> HOLogic.boolT)
   38.38      val Sinduct = Rules.SPEC (tych P) Sinduction
   38.39 @@ -843,7 +843,7 @@
   38.40      val proved_cases = map (prove_case fconst thy) tasks
   38.41      val v =
   38.42        Free (singleton
   38.43 -        (Name.variant_list (List.foldr OldTerm.add_term_names [] (map concl proved_cases))) "v",
   38.44 +        (Name.variant_list (List.foldr Misc_Legacy.add_term_names [] (map concl proved_cases))) "v",
   38.45            domain)
   38.46      val vtyped = tych v
   38.47      val substs = map (Rules.SYM o Rules.ASSUME o tych o (curry HOLogic.mk_eq v)) pats
    39.1 --- a/src/HOL/Tools/TFL/usyntax.ML	Wed Aug 10 18:02:16 2011 -0700
    39.2 +++ b/src/HOL/Tools/TFL/usyntax.ML	Wed Aug 10 18:07:32 2011 -0700
    39.3 @@ -112,7 +112,7 @@
    39.4  
    39.5  val is_vartype = can dest_vtype;
    39.6  
    39.7 -val type_vars  = map mk_prim_vartype o OldTerm.typ_tvars
    39.8 +val type_vars  = map mk_prim_vartype o Misc_Legacy.typ_tvars
    39.9  fun type_varsl L = distinct (op =) (fold (curry op @ o type_vars) L []);
   39.10  
   39.11  val alpha  = mk_vartype "'a"
   39.12 @@ -142,7 +142,7 @@
   39.13  
   39.14  
   39.15  
   39.16 -val type_vars_in_term = map mk_prim_vartype o OldTerm.term_tvars;
   39.17 +val type_vars_in_term = map mk_prim_vartype o Misc_Legacy.term_tvars;
   39.18  
   39.19  
   39.20  
   39.21 @@ -319,7 +319,7 @@
   39.22  
   39.23  
   39.24  (* Need to reverse? *)
   39.25 -fun gen_all tm = list_mk_forall(OldTerm.term_frees tm, tm);
   39.26 +fun gen_all tm = list_mk_forall(Misc_Legacy.term_frees tm, tm);
   39.27  
   39.28  (* Destructing a cterm to a list of Terms *)
   39.29  fun strip_comb tm =
    40.1 --- a/src/HOL/Tools/choice_specification.ML	Wed Aug 10 18:02:16 2011 -0700
    40.2 +++ b/src/HOL/Tools/choice_specification.ML	Wed Aug 10 18:07:32 2011 -0700
    40.3 @@ -18,7 +18,7 @@
    40.4  
    40.5  fun close_form t =
    40.6      fold_rev (fn (s, T) => fn t => HOLogic.mk_all (s, T, t))
    40.7 -             (map dest_Free (OldTerm.term_frees t)) t
    40.8 +             (map dest_Free (Misc_Legacy.term_frees t)) t
    40.9  
   40.10  local
   40.11      fun mk_definitional [] arg = arg
   40.12 @@ -122,7 +122,7 @@
   40.13  
   40.14          fun proc_single prop =
   40.15              let
   40.16 -                val frees = OldTerm.term_frees prop
   40.17 +                val frees = Misc_Legacy.term_frees prop
   40.18                  val _ = forall (fn v => Sign.of_sort thy (type_of v,HOLogic.typeS)) frees
   40.19                    orelse error "Specificaton: Only free variables of sort 'type' allowed"
   40.20                  val prop_closed = close_form prop
    41.1 --- a/src/HOL/Tools/cnf_funcs.ML	Wed Aug 10 18:02:16 2011 -0700
    41.2 +++ b/src/HOL/Tools/cnf_funcs.ML	Wed Aug 10 18:07:32 2011 -0700
    41.3 @@ -511,7 +511,7 @@
    41.4              NONE
    41.5        in
    41.6          Int.max (max, the_default 0 idx)
    41.7 -      end) (OldTerm.term_frees simp) 0)
    41.8 +      end) (Misc_Legacy.term_frees simp) 0)
    41.9      (* finally, convert to definitional CNF (this should preserve the simplification) *)
   41.10      val cnfx_thm = make_under_quantifiers ctxt make_cnfx_thm_from_nnf simp
   41.11  (*###
    42.1 --- a/src/HOL/Tools/inductive_codegen.ML	Wed Aug 10 18:02:16 2011 -0700
    42.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Wed Aug 10 18:07:32 2011 -0700
    42.3 @@ -141,7 +141,7 @@
    42.4      (fn (m, rnd) => string_of_mode m ^
    42.5         (if rnd then " (random)" else "")) ms)) modes));
    42.6  
    42.7 -val term_vs = map (fst o fst o dest_Var) o OldTerm.term_vars;
    42.8 +val term_vs = map (fst o fst o dest_Var) o Misc_Legacy.term_vars;
    42.9  val terms_vs = distinct (op =) o maps term_vs;
   42.10  
   42.11  (** collect all Vars in a term (with duplicates!) **)
    43.1 --- a/src/HOL/Tools/record.ML	Wed Aug 10 18:02:16 2011 -0700
    43.2 +++ b/src/HOL/Tools/record.ML	Wed Aug 10 18:07:32 2011 -0700
    43.3 @@ -1512,7 +1512,7 @@
    43.4    let
    43.5      val ctxt' = fold (Variable.declare_typ o TFree) env ctxt;
    43.6      val T = Syntax.read_typ ctxt' raw_T;
    43.7 -    val env' = OldTerm.add_typ_tfrees (T, env);
    43.8 +    val env' = Misc_Legacy.add_typ_tfrees (T, env);
    43.9    in (T, env') end;
   43.10  
   43.11  fun cert_typ ctxt raw_T env =
   43.12 @@ -1520,7 +1520,7 @@
   43.13      val thy = Proof_Context.theory_of ctxt;
   43.14      val T = Type.no_tvars (Sign.certify_typ thy raw_T)
   43.15        handle TYPE (msg, _, _) => error msg;
   43.16 -    val env' = OldTerm.add_typ_tfrees (T, env);
   43.17 +    val env' = Misc_Legacy.add_typ_tfrees (T, env);
   43.18    in (T, env') end;
   43.19  
   43.20  
    44.1 --- a/src/HOL/Tools/refute.ML	Wed Aug 10 18:02:16 2011 -0700
    44.2 +++ b/src/HOL/Tools/refute.ML	Wed Aug 10 18:07:32 2011 -0700
    44.3 @@ -403,7 +403,7 @@
    44.4  fun close_form t =
    44.5    let
    44.6      (* (Term.indexname * Term.typ) list *)
    44.7 -    val vars = sort_wrt (fst o fst) (map dest_Var (OldTerm.term_vars t))
    44.8 +    val vars = sort_wrt (fst o fst) (map dest_Var (Misc_Legacy.term_vars t))
    44.9    in
   44.10      fold (fn ((x, i), T) => fn t' =>
   44.11        Term.all T $ Abs (x, T, abstract_over (Var ((x, i), T), t'))) vars t
   44.12 @@ -1212,7 +1212,7 @@
   44.13  
   44.14      (* existential closure over schematic variables *)
   44.15      (* (Term.indexname * Term.typ) list *)
   44.16 -    val vars = sort_wrt (fst o fst) (map dest_Var (OldTerm.term_vars t))
   44.17 +    val vars = sort_wrt (fst o fst) (map dest_Var (Misc_Legacy.term_vars t))
   44.18      (* Term.term *)
   44.19      val ex_closure = fold (fn ((x, i), T) => fn t' =>
   44.20        HOLogic.exists_const T $
    45.1 --- a/src/HOL/Tools/split_rule.ML	Wed Aug 10 18:02:16 2011 -0700
    45.2 +++ b/src/HOL/Tools/split_rule.ML	Wed Aug 10 18:07:32 2011 -0700
    45.3 @@ -88,7 +88,7 @@
    45.4  
    45.5  (*curries ALL function variables occurring in a rule's conclusion*)
    45.6  fun split_rule rl =
    45.7 -  fold_rev split_rule_var' (OldTerm.term_vars (concl_of rl)) rl
    45.8 +  fold_rev split_rule_var' (Misc_Legacy.term_vars (concl_of rl)) rl
    45.9    |> remove_internal_split
   45.10    |> Drule.export_without_context;
   45.11  
    46.1 --- a/src/Pure/Concurrent/bash.ML	Wed Aug 10 18:02:16 2011 -0700
    46.2 +++ b/src/Pure/Concurrent/bash.ML	Wed Aug 10 18:07:32 2011 -0700
    46.3 @@ -73,7 +73,7 @@
    46.4        in () end;
    46.5  
    46.6      fun cleanup () =
    46.7 -     (Simple_Thread.interrupt system_thread;
    46.8 +     (Simple_Thread.interrupt_unsynchronized system_thread;
    46.9        try File.rm script_path;
   46.10        try File.rm output_path;
   46.11        try File.rm pid_path);
    47.1 --- a/src/Pure/Concurrent/future.ML	Wed Aug 10 18:02:16 2011 -0700
    47.2 +++ b/src/Pure/Concurrent/future.ML	Wed Aug 10 18:07:32 2011 -0700
    47.3 @@ -39,9 +39,13 @@
    47.4    val task_of: 'a future -> Task_Queue.task
    47.5    val peek: 'a future -> 'a Exn.result option
    47.6    val is_finished: 'a future -> bool
    47.7 -  val forks:
    47.8 -    {name: string, group: Task_Queue.group option, deps: Task_Queue.task list, pri: int} ->
    47.9 -      (unit -> 'a) list -> 'a future list
   47.10 +  val interruptible_task: ('a -> 'b) -> 'a -> 'b
   47.11 +  val cancel_group: Task_Queue.group -> unit
   47.12 +  val cancel: 'a future -> unit
   47.13 +  type fork_params =
   47.14 +   {name: string, group: Task_Queue.group option, deps: Task_Queue.task list,
   47.15 +    pri: int, interrupts: bool}
   47.16 +  val forks: fork_params -> (unit -> 'a) list -> 'a future list
   47.17    val fork_pri: int -> (unit -> 'a) -> 'a future
   47.18    val fork: (unit -> 'a) -> 'a future
   47.19    val join_results: 'a future list -> 'a Exn.result list
   47.20 @@ -49,16 +53,11 @@
   47.21    val join: 'a future -> 'a
   47.22    val value: 'a -> 'a future
   47.23    val map: ('a -> 'b) -> 'a future -> 'b future
   47.24 -  val cond_forks:
   47.25 -    {name: string, group: Task_Queue.group option, deps: Task_Queue.task list, pri: int} ->
   47.26 -      (unit -> 'a) list -> 'a future list
   47.27 +  val cond_forks: fork_params -> (unit -> 'a) list -> 'a future list
   47.28    val promise_group: Task_Queue.group -> 'a future
   47.29    val promise: unit -> 'a future
   47.30    val fulfill_result: 'a future -> 'a Exn.result -> unit
   47.31    val fulfill: 'a future -> 'a -> unit
   47.32 -  val interruptible_task: ('a -> 'b) -> 'a -> 'b
   47.33 -  val cancel_group: Task_Queue.group -> unit
   47.34 -  val cancel: 'a future -> unit
   47.35    val shutdown: unit -> unit
   47.36    val status: (unit -> 'a) -> 'a
   47.37  end;
   47.38 @@ -74,8 +73,7 @@
   47.39    val tag = Universal.tag () : Task_Queue.task option Universal.tag;
   47.40  in
   47.41    fun worker_task () = the_default NONE (Thread.getLocal tag);
   47.42 -  fun setmp_worker_task data f x =
   47.43 -    Library.setmp_thread_data tag (worker_task ()) (SOME data) f x;
   47.44 +  fun setmp_worker_task task f x = setmp_thread_data tag (worker_task ()) (SOME task) f x;
   47.45  end;
   47.46  
   47.47  val worker_group = Option.map Task_Queue.group_of_task o worker_task;
   47.48 @@ -107,19 +105,6 @@
   47.49  fun peek x = Single_Assignment.peek (result_of x);
   47.50  fun is_finished x = is_some (peek x);
   47.51  
   47.52 -fun assign_result group result res =
   47.53 -  let
   47.54 -    val _ = Single_Assignment.assign result res
   47.55 -      handle exn as Fail _ =>
   47.56 -        (case Single_Assignment.peek result of
   47.57 -          SOME (Exn.Exn e) => reraise (if Exn.is_interrupt e then e else exn)
   47.58 -        | _ => reraise exn);
   47.59 -    val ok =
   47.60 -      (case the (Single_Assignment.peek result) of
   47.61 -        Exn.Exn exn => (Task_Queue.cancel_group group exn; false)
   47.62 -      | Exn.Res _ => true);
   47.63 -  in ok end;
   47.64 -
   47.65  
   47.66  
   47.67  (** scheduling **)
   47.68 @@ -173,23 +158,16 @@
   47.69    fold (fn (_, state_ref) => fn i => if ! state_ref = state then i + 1 else i) (! workers) 0;
   47.70  
   47.71  
   47.72 -(* execute future jobs *)
   47.73 +(* cancellation primitives *)
   47.74  
   47.75 -fun future_job group (e: unit -> 'a) =
   47.76 -  let
   47.77 -    val result = Single_Assignment.var "future" : 'a result;
   47.78 -    val pos = Position.thread_data ();
   47.79 -    fun job ok =
   47.80 -      let
   47.81 -        val res =
   47.82 -          if ok then
   47.83 -            Exn.capture (fn () =>
   47.84 -              Multithreading.with_attributes Multithreading.private_interrupts
   47.85 -                (fn _ => Position.setmp_thread_data pos e ()) before
   47.86 -              Multithreading.interrupted ()) ()
   47.87 -          else Exn.interrupt_exn;
   47.88 -      in assign_result group result res end;
   47.89 -  in (result, job) end;
   47.90 +fun interruptible_task f x =
   47.91 +  if Multithreading.available then
   47.92 +    Multithreading.with_attributes
   47.93 +      (if is_some (worker_task ())
   47.94 +       then Multithreading.private_interrupts
   47.95 +       else Multithreading.public_interrupts)
   47.96 +      (fn _ => f x)
   47.97 +  else interruptible f x;
   47.98  
   47.99  fun cancel_now group = (*requires SYNCHRONIZED*)
  47.100    Task_Queue.cancel (! queue) group;
  47.101 @@ -198,7 +176,10 @@
  47.102   (Unsynchronized.change canceled (insert Task_Queue.eq_group group);
  47.103    broadcast scheduler_event);
  47.104  
  47.105 -fun execute (task, jobs) =
  47.106 +
  47.107 +(* worker threads *)
  47.108 +
  47.109 +fun worker_exec (task, jobs) =
  47.110    let
  47.111      val group = Task_Queue.group_of_task task;
  47.112      val valid = not (Task_Queue.is_canceled group);
  47.113 @@ -215,6 +196,7 @@
  47.114      val _ = SYNCHRONIZED "finish" (fn () =>
  47.115        let
  47.116          val maximal = Unsynchronized.change_result queue (Task_Queue.finish task);
  47.117 +        val _ = Exn.capture Multithreading.interrupted ();
  47.118          val _ =
  47.119            if ok then ()
  47.120            else if cancel_now group then ()
  47.121 @@ -224,9 +206,6 @@
  47.122        in () end);
  47.123    in () end;
  47.124  
  47.125 -
  47.126 -(* worker threads *)
  47.127 -
  47.128  fun worker_wait active cond = (*requires SYNCHRONIZED*)
  47.129    let
  47.130      val state =
  47.131 @@ -253,7 +232,7 @@
  47.132  fun worker_loop name =
  47.133    (case SYNCHRONIZED name (fn () => worker_next ()) of
  47.134      NONE => ()
  47.135 -  | SOME work => (Exn.capture Multithreading.interrupted (); execute work; worker_loop name));
  47.136 +  | SOME work => (Exn.capture Multithreading.interrupted (); worker_exec work; worker_loop name));
  47.137  
  47.138  fun worker_start name = (*requires SYNCHRONIZED*)
  47.139    Unsynchronized.change workers (cons (Simple_Thread.fork false (fn () => worker_loop name),
  47.140 @@ -397,9 +376,58 @@
  47.141  
  47.142  (** futures **)
  47.143  
  47.144 +(* cancellation *)
  47.145 +
  47.146 +(*cancel: present and future group members will be interrupted eventually*)
  47.147 +fun cancel_group group = SYNCHRONIZED "cancel" (fn () =>
  47.148 + (if cancel_now group then () else cancel_later group;
  47.149 +  signal work_available; scheduler_check ()));
  47.150 +
  47.151 +fun cancel x = cancel_group (Task_Queue.group_of_task (task_of x));
  47.152 +
  47.153 +
  47.154 +(* future jobs *)
  47.155 +
  47.156 +fun assign_result group result res =
  47.157 +  let
  47.158 +    val _ = Single_Assignment.assign result res
  47.159 +      handle exn as Fail _ =>
  47.160 +        (case Single_Assignment.peek result of
  47.161 +          SOME (Exn.Exn e) => reraise (if Exn.is_interrupt e then e else exn)
  47.162 +        | _ => reraise exn);
  47.163 +    val ok =
  47.164 +      (case the (Single_Assignment.peek result) of
  47.165 +        Exn.Exn exn =>
  47.166 +          (SYNCHRONIZED "cancel" (fn () => Task_Queue.cancel_group group exn); false)
  47.167 +      | Exn.Res _ => true);
  47.168 +  in ok end;
  47.169 +
  47.170 +fun future_job group interrupts (e: unit -> 'a) =
  47.171 +  let
  47.172 +    val result = Single_Assignment.var "future" : 'a result;
  47.173 +    val pos = Position.thread_data ();
  47.174 +    fun job ok =
  47.175 +      let
  47.176 +        val res =
  47.177 +          if ok then
  47.178 +            Exn.capture (fn () =>
  47.179 +              Multithreading.with_attributes
  47.180 +                (if interrupts
  47.181 +                 then Multithreading.private_interrupts else Multithreading.no_interrupts)
  47.182 +                (fn _ => Position.setmp_thread_data pos e ()) before
  47.183 +              Multithreading.interrupted ()) ()
  47.184 +          else Exn.interrupt_exn;
  47.185 +      in assign_result group result res end;
  47.186 +  in (result, job) end;
  47.187 +
  47.188 +
  47.189  (* fork *)
  47.190  
  47.191 -fun forks {name, group, deps, pri} es =
  47.192 +type fork_params =
  47.193 + {name: string, group: Task_Queue.group option, deps: Task_Queue.task list,
  47.194 +  pri: int, interrupts: bool};
  47.195 +
  47.196 +fun forks ({name, group, deps, pri, interrupts}: fork_params) es =
  47.197    if null es then []
  47.198    else
  47.199      let
  47.200 @@ -409,7 +437,7 @@
  47.201          | SOME grp => grp);
  47.202        fun enqueue e queue =
  47.203          let
  47.204 -          val (result, job) = future_job grp e;
  47.205 +          val (result, job) = future_job grp interrupts e;
  47.206            val (task, queue') = Task_Queue.enqueue name grp deps pri job queue;
  47.207            val future = Future {promised = false, task = task, result = result};
  47.208          in (future, queue') end;
  47.209 @@ -424,7 +452,9 @@
  47.210          in futures end)
  47.211      end;
  47.212  
  47.213 -fun fork_pri pri e = singleton (forks {name = "", group = NONE, deps = [], pri = pri}) e;
  47.214 +fun fork_pri pri e =
  47.215 +  singleton (forks {name = "", group = NONE, deps = [], pri = pri, interrupts = true}) e;
  47.216 +
  47.217  fun fork e = fork_pri 0 e;
  47.218  
  47.219  
  47.220 @@ -452,7 +482,8 @@
  47.221      | (SOME work, deps') => SOME (work, deps'));
  47.222  
  47.223  fun execute_work NONE = ()
  47.224 -  | execute_work (SOME (work, deps')) = (worker_joining (fn () => execute work); join_work deps')
  47.225 +  | execute_work (SOME (work, deps')) =
  47.226 +      (worker_joining (fn () => worker_exec work); join_work deps')
  47.227  and join_work deps =
  47.228    Multithreading.with_attributes Multithreading.no_interrupts
  47.229      (fn _ => execute_work (SYNCHRONIZED "join" (fn () => join_next deps)));
  47.230 @@ -475,7 +506,7 @@
  47.231  fun join x = Exn.release (join_result x);
  47.232  
  47.233  
  47.234 -(* fast-path versions -- bypassing full task management *)
  47.235 +(* fast-path versions -- bypassing task queue *)
  47.236  
  47.237  fun value (x: 'a) =
  47.238    let
  47.239 @@ -489,7 +520,7 @@
  47.240    let
  47.241      val task = task_of x;
  47.242      val group = Task_Queue.new_group (SOME (Task_Queue.group_of_task task));
  47.243 -    val (result, job) = future_job group (fn () => f (join x));
  47.244 +    val (result, job) = future_job group true (fn () => f (join x));
  47.245  
  47.246      val extended = SYNCHRONIZED "extend" (fn () =>
  47.247        (case Task_Queue.extend task job (! queue) of
  47.248 @@ -499,8 +530,8 @@
  47.249      if extended then Future {promised = false, task = task, result = result}
  47.250      else
  47.251        singleton
  47.252 -        (forks {name = "Future.map", group = SOME group,
  47.253 -          deps = [task], pri = Task_Queue.pri_of_task task})
  47.254 +        (forks {name = "Future.map", group = SOME group, deps = [task],
  47.255 +          pri = Task_Queue.pri_of_task task, interrupts = true})
  47.256          (fn () => f (join x))
  47.257    end;
  47.258  
  47.259 @@ -538,7 +569,7 @@
  47.260                SYNCHRONIZED "fulfill_result" (fn () =>
  47.261                  Unsynchronized.change_result queue
  47.262                    (Task_Queue.dequeue_passive (Thread.self ()) task));
  47.263 -          in if still_passive then execute (task, [job]) else () end);
  47.264 +          in if still_passive then worker_exec (task, [job]) else () end);
  47.265        val _ =
  47.266          if is_some (Single_Assignment.peek result) then ()
  47.267          else worker_waiting [task] (fn () => ignore (Single_Assignment.await result));
  47.268 @@ -547,25 +578,6 @@
  47.269  fun fulfill x res = fulfill_result x (Exn.Res res);
  47.270  
  47.271  
  47.272 -(* cancellation *)
  47.273 -
  47.274 -fun interruptible_task f x =
  47.275 -  if Multithreading.available then
  47.276 -    Multithreading.with_attributes
  47.277 -      (if is_some (worker_task ())
  47.278 -       then Multithreading.private_interrupts
  47.279 -       else Multithreading.public_interrupts)
  47.280 -      (fn _ => f x)
  47.281 -  else interruptible f x;
  47.282 -
  47.283 -(*cancel: present and future group members will be interrupted eventually*)
  47.284 -fun cancel_group group = SYNCHRONIZED "cancel" (fn () =>
  47.285 - (if cancel_now group then () else cancel_later group;
  47.286 -  signal work_available; scheduler_check ()));
  47.287 -
  47.288 -fun cancel x = cancel_group (Task_Queue.group_of_task (task_of x));
  47.289 -
  47.290 -
  47.291  (* shutdown *)
  47.292  
  47.293  fun shutdown () =
    48.1 --- a/src/Pure/Concurrent/par_list.ML	Wed Aug 10 18:02:16 2011 -0700
    48.2 +++ b/src/Pure/Concurrent/par_list.ML	Wed Aug 10 18:07:32 2011 -0700
    48.3 @@ -35,7 +35,7 @@
    48.4      let
    48.5        val group = Task_Queue.new_group (Future.worker_group ());
    48.6        val futures =
    48.7 -        Future.forks {name = name, group = SOME group, deps = [], pri = 0}
    48.8 +        Future.forks {name = name, group = SOME group, deps = [], pri = 0, interrupts = true}
    48.9            (map (fn x => fn () => f x) xs);
   48.10        val results = Future.join_results futures
   48.11          handle exn => (if Exn.is_interrupt exn then Future.cancel_group group else (); reraise exn);
    49.1 --- a/src/Pure/Concurrent/simple_thread.ML	Wed Aug 10 18:02:16 2011 -0700
    49.2 +++ b/src/Pure/Concurrent/simple_thread.ML	Wed Aug 10 18:07:32 2011 -0700
    49.3 @@ -8,7 +8,7 @@
    49.4  sig
    49.5    val attributes: bool -> Thread.threadAttribute list
    49.6    val fork: bool -> (unit -> unit) -> Thread.thread
    49.7 -  val interrupt: Thread.thread -> unit
    49.8 +  val interrupt_unsynchronized: Thread.thread -> unit
    49.9    val synchronized: string -> Mutex.mutex -> (unit -> 'a) -> 'a
   49.10  end;
   49.11  
   49.12 @@ -24,7 +24,7 @@
   49.13        body () handle exn => if Exn.is_interrupt exn then () else reraise exn),
   49.14      attributes interrupts);
   49.15  
   49.16 -fun interrupt thread = Thread.interrupt thread handle Thread _ => ();
   49.17 +fun interrupt_unsynchronized thread = Thread.interrupt thread handle Thread _ => ();
   49.18  
   49.19  
   49.20  (* basic synchronization *)
    50.1 --- a/src/Pure/Concurrent/task_queue.ML	Wed Aug 10 18:02:16 2011 -0700
    50.2 +++ b/src/Pure/Concurrent/task_queue.ML	Wed Aug 10 18:07:32 2011 -0700
    50.3 @@ -247,7 +247,7 @@
    50.4      val running =
    50.5        Tasks.fold (#1 #> get_job jobs #> (fn Running t => insert Thread.equal t | _ => I))
    50.6          (get_tasks groups (group_id group)) [];
    50.7 -    val _ = List.app Simple_Thread.interrupt running;
    50.8 +    val _ = List.app Simple_Thread.interrupt_unsynchronized running;
    50.9    in null running end;
   50.10  
   50.11  fun cancel_all (Queue {jobs, ...}) =
   50.12 @@ -262,7 +262,7 @@
   50.13          | _ => (groups, running))
   50.14        end;
   50.15      val (running_groups, running) = Task_Graph.fold cancel_job jobs ([], []);
   50.16 -    val _ = List.app Simple_Thread.interrupt running;
   50.17 +    val _ = List.app Simple_Thread.interrupt_unsynchronized running;
   50.18    in running_groups end;
   50.19  
   50.20  
    51.1 --- a/src/Pure/Concurrent/time_limit.ML	Wed Aug 10 18:02:16 2011 -0700
    51.2 +++ b/src/Pure/Concurrent/time_limit.ML	Wed Aug 10 18:07:32 2011 -0700
    51.3 @@ -30,12 +30,12 @@
    51.4        val main = Thread.self ();
    51.5        val timeout = Unsynchronized.ref false;
    51.6        val watchdog = Simple_Thread.fork true (fn () =>
    51.7 -        (OS.Process.sleep time; timeout := true; Thread.interrupt main));
    51.8 +        (OS.Process.sleep time; timeout := true; Simple_Thread.interrupt_unsynchronized main));
    51.9  
   51.10        val result =
   51.11          Exn.capture (fn () => Multithreading.with_attributes orig_atts (fn _ => f x)) ();
   51.12  
   51.13 -      val _ = Thread.interrupt watchdog handle Thread _ => ();
   51.14 +      val _ = Simple_Thread.interrupt_unsynchronized watchdog;
   51.15        val _ = while Thread.isActive watchdog do OS.Process.sleep wait_time;
   51.16  
   51.17        val test = Exn.capture Multithreading.interrupted ();
    52.1 --- a/src/Pure/IsaMakefile	Wed Aug 10 18:02:16 2011 -0700
    52.2 +++ b/src/Pure/IsaMakefile	Wed Aug 10 18:07:32 2011 -0700
    52.3 @@ -210,7 +210,6 @@
    52.4    Tools/xml_syntax.ML					\
    52.5    assumption.ML						\
    52.6    axclass.ML						\
    52.7 -  codegen.ML						\
    52.8    config.ML						\
    52.9    conjunction.ML					\
   52.10    consts.ML						\
   52.11 @@ -233,7 +232,6 @@
   52.12    morphism.ML						\
   52.13    name.ML						\
   52.14    net.ML						\
   52.15 -  old_term.ML						\
   52.16    pattern.ML						\
   52.17    primitive_defs.ML					\
   52.18    proofterm.ML						\
    53.1 --- a/src/Pure/PIDE/document.ML	Wed Aug 10 18:02:16 2011 -0700
    53.2 +++ b/src/Pure/PIDE/document.ML	Wed Aug 10 18:07:32 2011 -0700
    53.3 @@ -228,7 +228,7 @@
    53.4    ignore
    53.5      (singleton
    53.6        (Future.forks {name = "Document.async_state",
    53.7 -        group = SOME (Task_Queue.new_group NONE), deps = [], pri = 0})
    53.8 +        group = SOME (Task_Queue.new_group NONE), deps = [], pri = 0, interrupts = true})
    53.9        (fn () =>
   53.10          Toplevel.setmp_thread_position tr
   53.11            (fn () => Toplevel.print_state false st) ()));
   53.12 @@ -359,7 +359,8 @@
   53.13          | force_exec (SOME exec_id) = ignore (Lazy.force (the_exec state exec_id));
   53.14  
   53.15        val execution' = (* FIXME proper node deps *)
   53.16 -        Future.forks {name = "Document.execute", group = NONE, deps = [], pri = 1}
   53.17 +        Future.forks
   53.18 +          {name = "Document.execute", group = NONE, deps = [], pri = 1, interrupts = true}
   53.19            [fn () =>
   53.20              node_names_of version |> List.app (fn name =>
   53.21                fold_entries NONE (fn (_, exec) => fn () => force_exec exec)
    54.1 --- a/src/Pure/Proof/reconstruct.ML	Wed Aug 10 18:02:16 2011 -0700
    54.2 +++ b/src/Pure/Proof/reconstruct.ML	Wed Aug 10 18:07:32 2011 -0700
    54.3 @@ -288,9 +288,9 @@
    54.4      val _ = message "Collecting constraints...";
    54.5      val (t, prf, cs, env, _) = make_constraints_cprf thy
    54.6        (Envir.empty (Proofterm.maxidx_proof cprf ~1)) cprf';
    54.7 -    val cs' = map (fn p => (true, p, uncurry (union (op =)) 
    54.8 -        (pairself (map (fst o dest_Var) o OldTerm.term_vars) p)))
    54.9 -      (map (pairself (Envir.norm_term env)) ((t, prop')::cs));
   54.10 +    val cs' =
   54.11 +      map (pairself (Envir.norm_term env)) ((t, prop') :: cs)
   54.12 +      |> map (fn p => (true, p, Term.add_var_names (#1 p) (Term.add_var_names (#2 p) [])));
   54.13      val _ = message ("Solving remaining constraints (" ^ string_of_int (length cs') ^ ") ...");
   54.14      val env' = solve thy cs' env
   54.15    in
    55.1 --- a/src/Pure/ROOT.ML	Wed Aug 10 18:02:16 2011 -0700
    55.2 +++ b/src/Pure/ROOT.ML	Wed Aug 10 18:07:32 2011 -0700
    55.3 @@ -119,7 +119,6 @@
    55.4  use "term_ord.ML";
    55.5  use "term_subst.ML";
    55.6  use "term_xml.ML";
    55.7 -use "old_term.ML";
    55.8  use "General/name_space.ML";
    55.9  use "sorts.ML";
   55.10  use "type.ML";
   55.11 @@ -279,8 +278,6 @@
   55.12  use "Tools/find_theorems.ML";
   55.13  use "Tools/find_consts.ML";
   55.14  
   55.15 -use "codegen.ML";
   55.16 -
   55.17  
   55.18  (* configuration for Proof General *)
   55.19  
    56.1 --- a/src/Pure/Syntax/syntax.ML	Wed Aug 10 18:02:16 2011 -0700
    56.2 +++ b/src/Pure/Syntax/syntax.ML	Wed Aug 10 18:07:32 2011 -0700
    56.3 @@ -489,7 +489,7 @@
    56.4  fun future_gram deps e =
    56.5    singleton
    56.6      (Future.cond_forks {name = "Syntax.gram", group = NONE,
    56.7 -      deps = map Future.task_of deps, pri = 0}) e;
    56.8 +      deps = map Future.task_of deps, pri = 0, interrupts = true}) e;
    56.9  
   56.10  datatype syntax =
   56.11    Syntax of {
    57.1 --- a/src/Pure/System/isabelle_system.ML	Wed Aug 10 18:02:16 2011 -0700
    57.2 +++ b/src/Pure/System/isabelle_system.ML	Wed Aug 10 18:07:32 2011 -0700
    57.3 @@ -96,7 +96,7 @@
    57.4          (_, 0) => f path
    57.5        | (out, _) => error (perhaps (try (unsuffix "\n")) out)));
    57.6  
    57.7 -fun bash_output_fifo script f =
    57.8 +fun bash_output_fifo script f =  (* FIXME blocks on Cygwin 1.7.x *)
    57.9    with_tmp_fifo (fn fifo =>
   57.10      uninterruptible (fn restore_attributes => fn () =>
   57.11        (case Bash.process (script ^ " > " ^ File.shell_path fifo ^ " &") of
    58.1 --- a/src/Pure/Thy/thy_info.ML	Wed Aug 10 18:02:16 2011 -0700
    58.2 +++ b/src/Pure/Thy/thy_info.ML	Wed Aug 10 18:07:32 2011 -0700
    58.3 @@ -205,7 +205,9 @@
    58.4  
    58.5              val future =
    58.6                singleton
    58.7 -                (Future.forks {name = "theory:" ^ name, group = NONE, deps = task_deps, pri = 0})
    58.8 +                (Future.forks
    58.9 +                  {name = "theory:" ^ name, group = NONE, deps = task_deps, pri = 0,
   58.10 +                    interrupts = true})
   58.11                  (fn () =>
   58.12                    (case map_filter failed deps of
   58.13                      [] => body (map (#1 o Future.join o get) parents)
    59.1 --- a/src/Pure/Thy/thy_load.ML	Wed Aug 10 18:02:16 2011 -0700
    59.2 +++ b/src/Pure/Thy/thy_load.ML	Wed Aug 10 18:07:32 2011 -0700
    59.3 @@ -189,7 +189,7 @@
    59.4  
    59.5      val present =
    59.6        singleton (Future.cond_forks {name = "Outer_Syntax.present:" ^ name, group = NONE,
    59.7 -        deps = map Future.task_of results, pri = 0})
    59.8 +        deps = map Future.task_of results, pri = 0, interrupts = true})
    59.9        (fn () =>
   59.10          Thy_Output.present_thy (#1 lexs) Keyword.command_tags
   59.11            (Outer_Syntax.is_markup outer_syntax)
    60.1 --- a/src/Pure/codegen.ML	Wed Aug 10 18:02:16 2011 -0700
    60.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    60.3 @@ -1,1049 +0,0 @@
    60.4 -(*  Title:      Pure/codegen.ML
    60.5 -    Author:     Stefan Berghofer, TU Muenchen
    60.6 -
    60.7 -Generic code generator.
    60.8 -*)
    60.9 -
   60.10 -signature CODEGEN =
   60.11 -sig
   60.12 -  val quiet_mode : bool Unsynchronized.ref
   60.13 -  val message : string -> unit
   60.14 -  val margin : int Unsynchronized.ref
   60.15 -  val string_of : Pretty.T -> string
   60.16 -  val str : string -> Pretty.T
   60.17 -
   60.18 -  datatype 'a mixfix =
   60.19 -      Arg
   60.20 -    | Ignore
   60.21 -    | Module
   60.22 -    | Pretty of Pretty.T
   60.23 -    | Quote of 'a;
   60.24 -
   60.25 -  type deftab
   60.26 -  type node
   60.27 -  type codegr
   60.28 -  type 'a codegen
   60.29 -
   60.30 -  val add_codegen: string -> term codegen -> theory -> theory
   60.31 -  val add_tycodegen: string -> typ codegen -> theory -> theory
   60.32 -  val add_preprocessor: (theory -> thm list -> thm list) -> theory -> theory
   60.33 -  val preprocess: theory -> thm list -> thm list
   60.34 -  val preprocess_term: theory -> term -> term
   60.35 -  val print_codegens: theory -> unit
   60.36 -  val generate_code: theory -> string list -> string list -> string -> (string * string) list ->
   60.37 -    (string * string) list * codegr
   60.38 -  val generate_code_i: theory -> string list -> string list -> string -> (string * term) list ->
   60.39 -    (string * string) list * codegr
   60.40 -  val assoc_const: string * (term mixfix list *
   60.41 -    (string * string) list) -> theory -> theory
   60.42 -  val assoc_const_i: (string * typ) * (term mixfix list *
   60.43 -    (string * string) list) -> theory -> theory
   60.44 -  val assoc_type: xstring * (typ mixfix list *
   60.45 -    (string * string) list) -> theory -> theory
   60.46 -  val get_assoc_code: theory -> string * typ ->
   60.47 -    (term mixfix list * (string * string) list) option
   60.48 -  val get_assoc_type: theory -> string ->
   60.49 -    (typ mixfix list * (string * string) list) option
   60.50 -  val codegen_error: codegr -> string -> string -> 'a
   60.51 -  val invoke_codegen: theory -> string list -> deftab -> string -> string -> bool ->
   60.52 -    term -> codegr -> Pretty.T * codegr
   60.53 -  val invoke_tycodegen: theory -> string list -> deftab -> string -> string -> bool ->
   60.54 -    typ -> codegr -> Pretty.T * codegr
   60.55 -  val mk_id: string -> string
   60.56 -  val mk_qual_id: string -> string * string -> string
   60.57 -  val mk_const_id: string -> string -> codegr -> (string * string) * codegr
   60.58 -  val get_const_id: codegr -> string -> string * string
   60.59 -  val mk_type_id: string -> string -> codegr -> (string * string) * codegr
   60.60 -  val get_type_id: codegr -> string -> string * string
   60.61 -  val thyname_of_type: theory -> string -> string
   60.62 -  val thyname_of_const: theory -> string -> string
   60.63 -  val rename_terms: term list -> term list
   60.64 -  val rename_term: term -> term
   60.65 -  val new_names: term -> string list -> string list
   60.66 -  val new_name: term -> string -> string
   60.67 -  val if_library: string list -> 'a -> 'a -> 'a
   60.68 -  val get_defn: theory -> deftab -> string -> typ ->
   60.69 -    ((typ * (string * thm)) * int option) option
   60.70 -  val is_instance: typ -> typ -> bool
   60.71 -  val parens: Pretty.T -> Pretty.T
   60.72 -  val mk_app: bool -> Pretty.T -> Pretty.T list -> Pretty.T
   60.73 -  val mk_tuple: Pretty.T list -> Pretty.T
   60.74 -  val mk_let: (Pretty.T * Pretty.T) list -> Pretty.T -> Pretty.T
   60.75 -  val eta_expand: term -> term list -> int -> term
   60.76 -  val strip_tname: string -> string
   60.77 -  val mk_type: bool -> typ -> Pretty.T
   60.78 -  val mk_term_of: codegr -> string -> bool -> typ -> Pretty.T
   60.79 -  val mk_gen: codegr -> string -> bool -> string list -> string -> typ -> Pretty.T
   60.80 -  val poke_test_fn: (int -> term list option) -> unit
   60.81 -  val poke_eval_fn: (unit -> term) -> unit
   60.82 -  val test_term: Proof.context -> term -> int -> term list option
   60.83 -  val eval_term: Proof.context -> term -> term
   60.84 -  val evaluation_conv: Proof.context -> conv
   60.85 -  val parse_mixfix: (string -> 'a) -> string -> 'a mixfix list
   60.86 -  val quotes_of: 'a mixfix list -> 'a list
   60.87 -  val num_args_of: 'a mixfix list -> int
   60.88 -  val replace_quotes: 'b list -> 'a mixfix list -> 'b mixfix list
   60.89 -  val mk_deftab: theory -> deftab
   60.90 -  val map_unfold: (simpset -> simpset) -> theory -> theory
   60.91 -  val add_unfold: thm -> theory -> theory
   60.92 -  val del_unfold: thm -> theory -> theory
   60.93 -
   60.94 -  val get_node: codegr -> string -> node
   60.95 -  val add_edge: string * string -> codegr -> codegr
   60.96 -  val add_edge_acyclic: string * string -> codegr -> codegr
   60.97 -  val del_nodes: string list -> codegr -> codegr
   60.98 -  val map_node: string -> (node -> node) -> codegr -> codegr
   60.99 -  val new_node: string * node -> codegr -> codegr
  60.100 -
  60.101 -  val setup: theory -> theory
  60.102 -end;
  60.103 -
  60.104 -structure Codegen : CODEGEN =
  60.105 -struct
  60.106 -
  60.107 -val quiet_mode = Unsynchronized.ref true;
  60.108 -fun message s = if !quiet_mode then () else writeln s;
  60.109 -
  60.110 -val margin = Unsynchronized.ref 80;
  60.111 -
  60.112 -fun string_of p = Print_Mode.setmp [] (Pretty.string_of_margin (!margin)) p;
  60.113 -
  60.114 -val str = Print_Mode.setmp [] Pretty.str;
  60.115 -
  60.116 -(**** Mixfix syntax ****)
  60.117 -
  60.118 -datatype 'a mixfix =
  60.119 -    Arg
  60.120 -  | Ignore
  60.121 -  | Module
  60.122 -  | Pretty of Pretty.T
  60.123 -  | Quote of 'a;
  60.124 -
  60.125 -fun is_arg Arg = true
  60.126 -  | is_arg Ignore = true
  60.127 -  | is_arg _ = false;
  60.128 -
  60.129 -fun quotes_of [] = []
  60.130 -  | quotes_of (Quote q :: ms) = q :: quotes_of ms
  60.131 -  | quotes_of (_ :: ms) = quotes_of ms;
  60.132 -
  60.133 -fun args_of [] xs = ([], xs)
  60.134 -  | args_of (Arg :: ms) (x :: xs) = apfst (cons x) (args_of ms xs)
  60.135 -  | args_of (Ignore :: ms) (_ :: xs) = args_of ms xs
  60.136 -  | args_of (_ :: ms) xs = args_of ms xs;
  60.137 -
  60.138 -fun num_args_of x = length (filter is_arg x);
  60.139 -
  60.140 -
  60.141 -(**** theory data ****)
  60.142 -
  60.143 -(* preprocessed definition table *)
  60.144 -
  60.145 -type deftab =
  60.146 -  (typ *              (* type of constant *)
  60.147 -    (string *         (* name of theory containing definition of constant *)
  60.148 -      thm))           (* definition theorem *)
  60.149 -  list Symtab.table;
  60.150 -
  60.151 -(* code dependency graph *)
  60.152 -
  60.153 -type nametab = (string * string) Symtab.table * unit Symtab.table;
  60.154 -
  60.155 -fun merge_nametabs ((tab, used) : nametab, (tab', used')) =
  60.156 -  (Symtab.merge op = (tab, tab'), Symtab.merge op = (used, used'));
  60.157 -
  60.158 -type node =
  60.159 -  (exn option *    (* slot for arbitrary data *)
  60.160 -   string *        (* name of structure containing piece of code *)
  60.161 -   string);        (* piece of code *)
  60.162 -
  60.163 -type codegr =
  60.164 -  node Graph.T *
  60.165 -  (nametab *       (* table for assigned constant names *)
  60.166 -   nametab);       (* table for assigned type names *)
  60.167 -
  60.168 -val emptygr : codegr = (Graph.empty,
  60.169 -  ((Symtab.empty, Symtab.empty), (Symtab.empty, Symtab.empty)));
  60.170 -
  60.171 -(* type of code generators *)
  60.172 -
  60.173 -type 'a codegen =
  60.174 -  theory ->      (* theory in which generate_code was called *)
  60.175 -  string list -> (* mode *)
  60.176 -  deftab ->      (* definition table (for efficiency) *)
  60.177 -  string ->      (* node name of caller (for recording dependencies) *)
  60.178 -  string ->      (* module name of caller (for modular code generation) *)
  60.179 -  bool ->        (* whether to parenthesize generated expression *)
  60.180 -  'a ->          (* item to generate code from *)
  60.181 -  codegr ->      (* code dependency graph *)
  60.182 -  (Pretty.T * codegr) option;
  60.183 -
  60.184 -
  60.185 -(* theory data *)
  60.186 -
  60.187 -structure CodegenData = Theory_Data
  60.188 -(
  60.189 -  type T =
  60.190 -    {codegens : (string * term codegen) list,
  60.191 -     tycodegens : (string * typ codegen) list,
  60.192 -     consts : ((string * typ) * (term mixfix list * (string * string) list)) list,
  60.193 -     types : (string * (typ mixfix list * (string * string) list)) list,
  60.194 -     preprocs: (stamp * (theory -> thm list -> thm list)) list,
  60.195 -     modules: codegr Symtab.table};
  60.196 -
  60.197 -  val empty =
  60.198 -    {codegens = [], tycodegens = [], consts = [], types = [],
  60.199 -     preprocs = [], modules = Symtab.empty};
  60.200 -  val extend = I;
  60.201 -
  60.202 -  fun merge
  60.203 -    ({codegens = codegens1, tycodegens = tycodegens1,
  60.204 -      consts = consts1, types = types1,
  60.205 -      preprocs = preprocs1, modules = modules1} : T,
  60.206 -     {codegens = codegens2, tycodegens = tycodegens2,
  60.207 -      consts = consts2, types = types2,
  60.208 -      preprocs = preprocs2, modules = modules2}) : T =
  60.209 -    {codegens = AList.merge (op =) (K true) (codegens1, codegens2),
  60.210 -     tycodegens = AList.merge (op =) (K true) (tycodegens1, tycodegens2),
  60.211 -     consts = AList.merge (op =) (K true) (consts1, consts2),
  60.212 -     types = AList.merge (op =) (K true) (types1, types2),
  60.213 -     preprocs = AList.merge (op =) (K true) (preprocs1, preprocs2),
  60.214 -     modules = Symtab.merge (K true) (modules1, modules2)};
  60.215 -);
  60.216 -
  60.217 -fun print_codegens thy =
  60.218 -  let val {codegens, tycodegens, ...} = CodegenData.get thy in
  60.219 -    Pretty.writeln (Pretty.chunks
  60.220 -      [Pretty.strs ("term code generators:" :: map fst codegens),
  60.221 -       Pretty.strs ("type code generators:" :: map fst tycodegens)])
  60.222 -  end;
  60.223 -
  60.224 -
  60.225 -
  60.226 -(**** access modules ****)
  60.227 -
  60.228 -fun get_modules thy = #modules (CodegenData.get thy);
  60.229 -
  60.230 -fun map_modules f thy =
  60.231 -  let val {codegens, tycodegens, consts, types, preprocs, modules} =
  60.232 -    CodegenData.get thy;
  60.233 -  in CodegenData.put {codegens = codegens, tycodegens = tycodegens,
  60.234 -    consts = consts, types = types, preprocs = preprocs,
  60.235 -    modules = f modules} thy
  60.236 -  end;
  60.237 -
  60.238 -
  60.239 -(**** add new code generators to theory ****)
  60.240 -
  60.241 -fun add_codegen name f thy =
  60.242 -  let val {codegens, tycodegens, consts, types, preprocs, modules} =
  60.243 -    CodegenData.get thy
  60.244 -  in (case AList.lookup (op =) codegens name of
  60.245 -      NONE => CodegenData.put {codegens = (name, f) :: codegens,
  60.246 -        tycodegens = tycodegens, consts = consts, types = types,
  60.247 -        preprocs = preprocs, modules = modules} thy
  60.248 -    | SOME _ => error ("Code generator " ^ name ^ " already declared"))
  60.249 -  end;
  60.250 -
  60.251 -fun add_tycodegen name f thy =
  60.252 -  let val {codegens, tycodegens, consts, types, preprocs, modules} =
  60.253 -    CodegenData.get thy
  60.254 -  in (case AList.lookup (op =) tycodegens name of
  60.255 -      NONE => CodegenData.put {tycodegens = (name, f) :: tycodegens,
  60.256 -        codegens = codegens, consts = consts, types = types,
  60.257 -        preprocs = preprocs, modules = modules} thy
  60.258 -    | SOME _ => error ("Code generator " ^ name ^ " already declared"))
  60.259 -  end;
  60.260 -
  60.261 -
  60.262 -(**** preprocessors ****)
  60.263 -
  60.264 -fun add_preprocessor p thy =
  60.265 -  let val {codegens, tycodegens, consts, types, preprocs, modules} =
  60.266 -    CodegenData.get thy
  60.267 -  in CodegenData.put {tycodegens = tycodegens,
  60.268 -    codegens = codegens, consts = consts, types = types,
  60.269 -    preprocs = (stamp (), p) :: preprocs,
  60.270 -    modules = modules} thy
  60.271 -  end;
  60.272 -
  60.273 -fun preprocess thy =
  60.274 -  let val {preprocs, ...} = CodegenData.get thy
  60.275 -  in fold (fn (_, f) => f thy) preprocs end;
  60.276 -
  60.277 -fun preprocess_term thy t =
  60.278 -  let
  60.279 -    val x = Free (singleton (Name.variant_list (OldTerm.add_term_names (t, []))) "x", fastype_of t);
  60.280 -    (* fake definition *)
  60.281 -    val eq = Skip_Proof.make_thm thy (Logic.mk_equals (x, t));
  60.282 -    fun err () = error "preprocess_term: bad preprocessor"
  60.283 -  in case map prop_of (preprocess thy [eq]) of
  60.284 -      [Const ("==", _) $ x' $ t'] => if x = x' then t' else err ()
  60.285 -    | _ => err ()
  60.286 -  end;
  60.287 -
  60.288 -structure UnfoldData = Theory_Data
  60.289 -(
  60.290 -  type T = simpset;
  60.291 -  val empty = empty_ss;
  60.292 -  val extend = I;
  60.293 -  val merge = merge_ss;
  60.294 -);
  60.295 -
  60.296 -val map_unfold = UnfoldData.map;
  60.297 -val add_unfold = map_unfold o Simplifier.add_simp;
  60.298 -val del_unfold = map_unfold o Simplifier.del_simp;
  60.299 -
  60.300 -fun unfold_preprocessor thy =
  60.301 -  let val ss = Simplifier.global_context thy (UnfoldData.get thy)
  60.302 -  in map (Thm.transfer thy #> Simplifier.full_simplify ss) end;
  60.303 -
  60.304 -
  60.305 -(**** associate constants with target language code ****)
  60.306 -
  60.307 -fun gen_assoc_const prep_const (raw_const, syn) thy =
  60.308 -  let
  60.309 -    val {codegens, tycodegens, consts, types, preprocs, modules} =
  60.310 -      CodegenData.get thy;
  60.311 -    val (cname, T) = prep_const thy raw_const;
  60.312 -  in
  60.313 -    if num_args_of (fst syn) > length (binder_types T) then
  60.314 -      error ("More arguments than in corresponding type of " ^ cname)
  60.315 -    else case AList.lookup (op =) consts (cname, T) of
  60.316 -      NONE => CodegenData.put {codegens = codegens,
  60.317 -        tycodegens = tycodegens,
  60.318 -        consts = ((cname, T), syn) :: consts,
  60.319 -        types = types, preprocs = preprocs,
  60.320 -        modules = modules} thy
  60.321 -    | SOME _ => error ("Constant " ^ cname ^ " already associated with code")
  60.322 -  end;
  60.323 -
  60.324 -val assoc_const_i = gen_assoc_const (K I);
  60.325 -val assoc_const = gen_assoc_const Code.read_bare_const;
  60.326 -
  60.327 -
  60.328 -(**** associate types with target language types ****)
  60.329 -
  60.330 -fun assoc_type (s, syn) thy =
  60.331 -  let
  60.332 -    val {codegens, tycodegens, consts, types, preprocs, modules} =
  60.333 -      CodegenData.get thy;
  60.334 -    val tc = Sign.intern_type thy s;
  60.335 -  in
  60.336 -    case Symtab.lookup (snd (#types (Type.rep_tsig (Sign.tsig_of thy)))) tc of
  60.337 -      SOME (Type.LogicalType i) =>
  60.338 -        if num_args_of (fst syn) > i then
  60.339 -          error ("More arguments than corresponding type constructor " ^ s)
  60.340 -        else
  60.341 -          (case AList.lookup (op =) types tc of
  60.342 -            NONE => CodegenData.put {codegens = codegens,
  60.343 -              tycodegens = tycodegens, consts = consts,
  60.344 -              types = (tc, syn) :: types,
  60.345 -              preprocs = preprocs, modules = modules} thy
  60.346 -          | SOME _ => error ("Type " ^ tc ^ " already associated with code"))
  60.347 -    | _ => error ("Not a type constructor: " ^ s)
  60.348 -  end;
  60.349 -
  60.350 -fun get_assoc_type thy = AList.lookup (op =) ((#types o CodegenData.get) thy);
  60.351 -
  60.352 -
  60.353 -(**** make valid ML identifiers ****)
  60.354 -
  60.355 -fun is_ascii_letdig x = Symbol.is_ascii_letter x orelse
  60.356 -  Symbol.is_ascii_digit x orelse Symbol.is_ascii_quasi x;
  60.357 -
  60.358 -fun dest_sym s =
  60.359 -  (case split_last (snd (take_prefix (fn c => c = "\\") (raw_explode s))) of
  60.360 -    ("<" :: "^" :: xs, ">") => (true, implode xs)
  60.361 -  | ("<" :: xs, ">") => (false, implode xs)
  60.362 -  | _ => raise Fail "dest_sym");
  60.363 -
  60.364 -fun mk_id s = if s = "" then "" else
  60.365 -  let
  60.366 -    fun check_str [] = []
  60.367 -      | check_str xs = (case take_prefix is_ascii_letdig xs of
  60.368 -          ([], " " :: zs) => check_str zs
  60.369 -        | ([], z :: zs) =>
  60.370 -          if size z = 1 then string_of_int (ord z) :: check_str zs
  60.371 -          else (case dest_sym z of
  60.372 -              (true, "isub") => check_str zs
  60.373 -            | (true, "isup") => "" :: check_str zs
  60.374 -            | (ctrl, s') => (if ctrl then "ctrl_" ^ s' else s') :: check_str zs)
  60.375 -        | (ys, zs) => implode ys :: check_str zs);
  60.376 -    val s' = space_implode "_" (maps (check_str o Symbol.explode) (Long_Name.explode s))
  60.377 -  in
  60.378 -    if Symbol.is_ascii_letter (hd (raw_explode s')) then s' else "id_" ^ s'
  60.379 -  end;
  60.380 -
  60.381 -fun mk_long_id (p as (tab, used)) module s =
  60.382 -  let
  60.383 -    fun find_name [] = raise Fail "mk_long_id"
  60.384 -      | find_name (ys :: yss) =
  60.385 -          let
  60.386 -            val s' = Long_Name.implode ys
  60.387 -            val s'' = Long_Name.append module s'
  60.388 -          in case Symtab.lookup used s'' of
  60.389 -              NONE => ((module, s'),
  60.390 -                (Symtab.update_new (s, (module, s')) tab,
  60.391 -                 Symtab.update_new (s'', ()) used))
  60.392 -            | SOME _ => find_name yss
  60.393 -          end
  60.394 -  in case Symtab.lookup tab s of
  60.395 -      NONE => find_name (Library.suffixes1 (Long_Name.explode s))
  60.396 -    | SOME name => (name, p)
  60.397 -  end;
  60.398 -
  60.399 -(* module:  module name for caller                                        *)
  60.400 -(* module': module name for callee                                        *)
  60.401 -(* if caller and callee reside in different modules, use qualified access *)
  60.402 -
  60.403 -fun mk_qual_id module (module', s) =
  60.404 -  if module = module' orelse module' = "" then s else module' ^ "." ^ s;
  60.405 -
  60.406 -fun mk_const_id module cname (gr, (tab1, tab2)) =
  60.407 -  let
  60.408 -    val ((module, s), tab1') = mk_long_id tab1 module cname
  60.409 -    val s' = mk_id s;
  60.410 -    val s'' = if ML_Syntax.is_reserved s' then s' ^ "_const" else s'
  60.411 -  in (((module, s'')), (gr, (tab1', tab2))) end;
  60.412 -
  60.413 -fun get_const_id (gr, (tab1, tab2)) cname =
  60.414 -  case Symtab.lookup (fst tab1) cname of
  60.415 -    NONE => error ("get_const_id: no such constant: " ^ quote cname)
  60.416 -  | SOME (module, s) =>
  60.417 -      let
  60.418 -        val s' = mk_id s;
  60.419 -        val s'' = if ML_Syntax.is_reserved s' then s' ^ "_const" else s'
  60.420 -      in (module, s'') end;
  60.421 -
  60.422 -fun mk_type_id module tyname (gr, (tab1, tab2)) =
  60.423 -  let
  60.424 -    val ((module, s), tab2') = mk_long_id tab2 module tyname
  60.425 -    val s' = mk_id s;
  60.426 -    val s'' = if ML_Syntax.is_reserved s' then s' ^ "_type" else s'
  60.427 -  in ((module, s''), (gr, (tab1, tab2'))) end;
  60.428 -
  60.429 -fun get_type_id (gr, (tab1, tab2)) tyname =
  60.430 -  case Symtab.lookup (fst tab2) tyname of
  60.431 -    NONE => error ("get_type_id: no such type: " ^ quote tyname)
  60.432 -  | SOME (module, s) =>
  60.433 -      let
  60.434 -        val s' = mk_id s;
  60.435 -        val s'' = if ML_Syntax.is_reserved s' then s' ^ "_type" else s'
  60.436 -      in (module, s'') end;
  60.437 -
  60.438 -fun get_type_id' f tab tyname = apsnd f (get_type_id tab tyname);
  60.439 -
  60.440 -fun get_node (gr, x) k = Graph.get_node gr k;
  60.441 -fun add_edge e (gr, x) = (Graph.add_edge e gr, x);
  60.442 -fun add_edge_acyclic e (gr, x) = (Graph.add_edge_acyclic e gr, x);
  60.443 -fun del_nodes ks (gr, x) = (Graph.del_nodes ks gr, x);
  60.444 -fun map_node k f (gr, x) = (Graph.map_node k f gr, x);
  60.445 -fun new_node p (gr, x) = (Graph.new_node p gr, x);
  60.446 -
  60.447 -fun thyname_of_type thy = #theory_name o Name_Space.the_entry (Sign.type_space thy);
  60.448 -fun thyname_of_const thy = #theory_name o Name_Space.the_entry (Sign.const_space thy);
  60.449 -
  60.450 -fun rename_terms ts =
  60.451 -  let
  60.452 -    val names = List.foldr OldTerm.add_term_names
  60.453 -      (map (fst o fst) (rev (fold Term.add_vars ts []))) ts;
  60.454 -    val reserved = filter ML_Syntax.is_reserved names;
  60.455 -    val (illegal, alt_names) = split_list (map_filter (fn s =>
  60.456 -      let val s' = mk_id s in if s = s' then NONE else SOME (s, s') end) names)
  60.457 -    val ps = (reserved @ illegal) ~~
  60.458 -      Name.variant_list names (map (suffix "'") reserved @ alt_names);
  60.459 -
  60.460 -    fun rename_id s = AList.lookup (op =) ps s |> the_default s;
  60.461 -
  60.462 -    fun rename (Var ((a, i), T)) = Var ((rename_id a, i), T)
  60.463 -      | rename (Free (a, T)) = Free (rename_id a, T)
  60.464 -      | rename (Abs (s, T, t)) = Abs (s, T, rename t)
  60.465 -      | rename (t $ u) = rename t $ rename u
  60.466 -      | rename t = t;
  60.467 -  in
  60.468 -    map rename ts
  60.469 -  end;
  60.470 -
  60.471 -val rename_term = hd o rename_terms o single;
  60.472 -
  60.473 -
  60.474 -(**** retrieve definition of constant ****)
  60.475 -
  60.476 -fun is_instance T1 T2 =
  60.477 -  Type.raw_instance (T1, if null (OldTerm.typ_tfrees T2) then T2 else Logic.varifyT_global T2);
  60.478 -
  60.479 -fun get_assoc_code thy (s, T) = Option.map snd (find_first (fn ((s', T'), _) =>
  60.480 -  s = s' andalso is_instance T T') (#consts (CodegenData.get thy)));
  60.481 -
  60.482 -fun get_aux_code mode xs = map_filter (fn (m, code) =>
  60.483 -  if m = "" orelse member (op =) mode m then SOME code else NONE) xs;
  60.484 -
  60.485 -fun dest_prim_def t =
  60.486 -  let
  60.487 -    val (lhs, rhs) = Logic.dest_equals t;
  60.488 -    val (c, args) = strip_comb lhs;
  60.489 -    val (s, T) = dest_Const c
  60.490 -  in if forall is_Var args then SOME (s, (T, (args, rhs))) else NONE
  60.491 -  end handle TERM _ => NONE;
  60.492 -
  60.493 -fun mk_deftab thy =
  60.494 -  let
  60.495 -    val axmss =
  60.496 -      map (fn thy' => (Context.theory_name thy', Theory.axiom_table thy'))
  60.497 -        (Theory.nodes_of thy);
  60.498 -    fun add_def thyname (name, t) =
  60.499 -      (case dest_prim_def t of
  60.500 -        NONE => I
  60.501 -      | SOME (s, (T, _)) => Symtab.map_default (s, [])
  60.502 -          (cons (T, (thyname, Thm.axiom thy name))));
  60.503 -  in
  60.504 -    fold (fn (thyname, axms) => Symtab.fold (add_def thyname) axms) axmss Symtab.empty
  60.505 -  end;
  60.506 -
  60.507 -fun prep_prim_def thy thm =
  60.508 -  let
  60.509 -    val prop = case preprocess thy [thm]
  60.510 -     of [thm'] => Thm.prop_of thm'
  60.511 -      | _ => error "mk_deftab: bad preprocessor"
  60.512 -  in ((Option.map o apsnd o apsnd)
  60.513 -    (fn (args, rhs) => split_last (rename_terms (args @ [rhs]))) o dest_prim_def) prop
  60.514 -  end;
  60.515 -
  60.516 -fun get_defn thy defs s T = (case Symtab.lookup defs s of
  60.517 -    NONE => NONE
  60.518 -  | SOME ds =>
  60.519 -      let val i = find_index (is_instance T o fst) ds
  60.520 -      in if i >= 0 then
  60.521 -          SOME (nth ds i, if length ds = 1 then NONE else SOME i)
  60.522 -        else NONE
  60.523 -      end);
  60.524 -
  60.525 -
  60.526 -(**** invoke suitable code generator for term / type ****)
  60.527 -
  60.528 -fun codegen_error (gr, _) dep s =
  60.529 -  error (s ^ "\nrequired by:\n" ^ commas (Graph.all_succs gr [dep]));
  60.530 -
  60.531 -fun invoke_codegen thy mode defs dep module brack t gr = (case get_first
  60.532 -   (fn (_, f) => f thy mode defs dep module brack t gr) (#codegens (CodegenData.get thy)) of
  60.533 -      NONE => codegen_error gr dep ("Unable to generate code for term:\n" ^
  60.534 -        Syntax.string_of_term_global thy t)
  60.535 -    | SOME x => x);
  60.536 -
  60.537 -fun invoke_tycodegen thy mode defs dep module brack T gr = (case get_first
  60.538 -   (fn (_, f) => f thy mode defs dep module brack T gr ) (#tycodegens (CodegenData.get thy)) of
  60.539 -      NONE => codegen_error gr dep ("Unable to generate code for type:\n" ^
  60.540 -        Syntax.string_of_typ_global thy T)
  60.541 -    | SOME x => x);
  60.542 -
  60.543 -
  60.544 -(**** code generator for mixfix expressions ****)
  60.545 -
  60.546 -fun parens p = Pretty.block [str "(", p, str ")"];
  60.547 -
  60.548 -fun pretty_fn [] p = [p]
  60.549 -  | pretty_fn (x::xs) p = str ("fn " ^ x ^ " =>") ::
  60.550 -      Pretty.brk 1 :: pretty_fn xs p;
  60.551 -
  60.552 -fun pretty_mixfix _ _ [] [] _ = []
  60.553 -  | pretty_mixfix module module' (Arg :: ms) (p :: ps) qs =
  60.554 -      p :: pretty_mixfix module module' ms ps qs
  60.555 -  | pretty_mixfix module module' (Ignore :: ms) ps qs =
  60.556 -      pretty_mixfix module module' ms ps qs
  60.557 -  | pretty_mixfix module module' (Module :: ms) ps qs =
  60.558 -      (if module <> module'
  60.559 -       then cons (str (module' ^ ".")) else I)
  60.560 -      (pretty_mixfix module module' ms ps qs)
  60.561 -  | pretty_mixfix module module' (Pretty p :: ms) ps qs =
  60.562 -      p :: pretty_mixfix module module' ms ps qs
  60.563 -  | pretty_mixfix module module' (Quote _ :: ms) ps (q :: qs) =
  60.564 -      q :: pretty_mixfix module module' ms ps qs;
  60.565 -
  60.566 -fun replace_quotes [] [] = []
  60.567 -  | replace_quotes xs (Arg :: ms) =
  60.568 -      Arg :: replace_quotes xs ms
  60.569 -  | replace_quotes xs (Ignore :: ms) =
  60.570 -      Ignore :: replace_quotes xs ms
  60.571 -  | replace_quotes xs (Module :: ms) =
  60.572 -      Module :: replace_quotes xs ms
  60.573 -  | replace_quotes xs (Pretty p :: ms) =
  60.574 -      Pretty p :: replace_quotes xs ms
  60.575 -  | replace_quotes (x::xs) (Quote _ :: ms) =
  60.576 -      Quote x :: replace_quotes xs ms;
  60.577 -
  60.578 -
  60.579 -(**** default code generators ****)
  60.580 -
  60.581 -fun eta_expand t ts i =
  60.582 -  let
  60.583 -    val k = length ts;
  60.584 -    val Ts = drop k (binder_types (fastype_of t));
  60.585 -    val j = i - k
  60.586 -  in
  60.587 -    List.foldr (fn (T, t) => Abs ("x", T, t))
  60.588 -      (list_comb (t, ts @ map Bound (j-1 downto 0))) (take j Ts)
  60.589 -  end;
  60.590 -
  60.591 -fun mk_app _ p [] = p
  60.592 -  | mk_app brack p ps = if brack then
  60.593 -       Pretty.block (str "(" ::
  60.594 -         separate (Pretty.brk 1) (p :: ps) @ [str ")"])
  60.595 -     else Pretty.block (separate (Pretty.brk 1) (p :: ps));
  60.596 -
  60.597 -fun new_names t xs = Name.variant_list
  60.598 -  (union (op =) (map (fst o fst o dest_Var) (OldTerm.term_vars t))
  60.599 -    (OldTerm.add_term_names (t, ML_Syntax.reserved_names))) (map mk_id xs);
  60.600 -
  60.601 -fun new_name t x = hd (new_names t [x]);
  60.602 -
  60.603 -fun if_library mode x y = if member (op =) mode "library" then x else y;
  60.604 -
  60.605 -fun default_codegen thy mode defs dep module brack t gr =
  60.606 -  let
  60.607 -    val (u, ts) = strip_comb t;
  60.608 -    fun codegens brack = fold_map (invoke_codegen thy mode defs dep module brack)
  60.609 -  in (case u of
  60.610 -      Var ((s, i), T) =>
  60.611 -        let
  60.612 -          val (ps, gr') = codegens true ts gr;
  60.613 -          val (_, gr'') = invoke_tycodegen thy mode defs dep module false T gr'
  60.614 -        in SOME (mk_app brack (str (s ^
  60.615 -           (if i=0 then "" else string_of_int i))) ps, gr'')
  60.616 -        end
  60.617 -
  60.618 -    | Free (s, T) =>
  60.619 -        let
  60.620 -          val (ps, gr') = codegens true ts gr;
  60.621 -          val (_, gr'') = invoke_tycodegen thy mode defs dep module false T gr'
  60.622 -        in SOME (mk_app brack (str s) ps, gr'') end
  60.623 -
  60.624 -    | Const (s, T) =>
  60.625 -      (case get_assoc_code thy (s, T) of
  60.626 -         SOME (ms, aux) =>
  60.627 -           let val i = num_args_of ms
  60.628 -           in if length ts < i then
  60.629 -               default_codegen thy mode defs dep module brack (eta_expand u ts i) gr 
  60.630 -             else
  60.631 -               let
  60.632 -                 val (ts1, ts2) = args_of ms ts;
  60.633 -                 val (ps1, gr1) = codegens false ts1 gr;
  60.634 -                 val (ps2, gr2) = codegens true ts2 gr1;
  60.635 -                 val (ps3, gr3) = codegens false (quotes_of ms) gr2;
  60.636 -                 val (_, gr4) = invoke_tycodegen thy mode defs dep module false
  60.637 -                   (funpow (length ts) (hd o tl o snd o dest_Type) T) gr3;
  60.638 -                 val (module', suffix) = (case get_defn thy defs s T of
  60.639 -                     NONE => (if_library mode (thyname_of_const thy s) module, "")
  60.640 -                   | SOME ((U, (module', _)), NONE) =>
  60.641 -                       (if_library mode module' module, "")
  60.642 -                   | SOME ((U, (module', _)), SOME i) =>
  60.643 -                       (if_library mode module' module, " def" ^ string_of_int i));
  60.644 -                 val node_id = s ^ suffix;
  60.645 -                 fun p module' = mk_app brack (Pretty.block
  60.646 -                   (pretty_mixfix module module' ms ps1 ps3)) ps2
  60.647 -               in SOME (case try (get_node gr4) node_id of
  60.648 -                   NONE => (case get_aux_code mode aux of
  60.649 -                       [] => (p module, gr4)
  60.650 -                     | xs => (p module', add_edge (node_id, dep) (new_node
  60.651 -                         (node_id, (NONE, module', cat_lines xs ^ "\n")) gr4)))
  60.652 -                 | SOME (_, module'', _) =>
  60.653 -                     (p module'', add_edge (node_id, dep) gr4))
  60.654 -               end
  60.655 -           end
  60.656 -       | NONE => (case get_defn thy defs s T of
  60.657 -           NONE => NONE
  60.658 -         | SOME ((U, (thyname, thm)), k) => (case prep_prim_def thy thm
  60.659 -            of SOME (_, (_, (args, rhs))) => let
  60.660 -               val module' = if_library mode thyname module;
  60.661 -               val suffix = (case k of NONE => "" | SOME i => " def" ^ string_of_int i);
  60.662 -               val node_id = s ^ suffix;
  60.663 -               val ((ps, def_id), gr') = gr |> codegens true ts
  60.664 -                 ||>> mk_const_id module' (s ^ suffix);
  60.665 -               val p = mk_app brack (str (mk_qual_id module def_id)) ps
  60.666 -             in SOME (case try (get_node gr') node_id of
  60.667 -                 NONE =>
  60.668 -                   let
  60.669 -                     val _ = message ("expanding definition of " ^ s);
  60.670 -                     val Ts = binder_types U;
  60.671 -                     val (args', rhs') =
  60.672 -                       if not (null args) orelse null Ts then (args, rhs) else
  60.673 -                         let val v = Free (new_name rhs "x", hd Ts)
  60.674 -                         in ([v], betapply (rhs, v)) end;
  60.675 -                     val (p', gr1) = invoke_codegen thy mode defs node_id module' false
  60.676 -                       rhs' (add_edge (node_id, dep)
  60.677 -                          (new_node (node_id, (NONE, "", "")) gr'));
  60.678 -                     val (xs, gr2) = codegens false args' gr1;
  60.679 -                     val (_, gr3) = invoke_tycodegen thy mode defs dep module false T gr2;
  60.680 -                     val (ty, gr4) = invoke_tycodegen thy mode defs node_id module' false U gr3;
  60.681 -                   in (p, map_node node_id (K (NONE, module', string_of
  60.682 -                       (Pretty.block (separate (Pretty.brk 1)
  60.683 -                         (if null args' then
  60.684 -                            [str ("val " ^ snd def_id ^ " :"), ty]
  60.685 -                          else str ("fun " ^ snd def_id) :: xs) @
  60.686 -                        [str " =", Pretty.brk 1, p', str ";"])) ^ "\n\n")) gr4)
  60.687 -                   end
  60.688 -               | SOME _ => (p, add_edge (node_id, dep) gr'))
  60.689 -             end
  60.690 -             | NONE => NONE)))
  60.691 -
  60.692 -    | Abs _ =>
  60.693 -      let
  60.694 -        val (bs, Ts) = ListPair.unzip (strip_abs_vars u);
  60.695 -        val t = strip_abs_body u
  60.696 -        val bs' = new_names t bs;
  60.697 -        val (ps, gr1) = codegens true ts gr;
  60.698 -        val (p, gr2) = invoke_codegen thy mode defs dep module false
  60.699 -          (subst_bounds (map Free (rev (bs' ~~ Ts)), t)) gr1;
  60.700 -      in
  60.701 -        SOME (mk_app brack (Pretty.block (str "(" :: pretty_fn bs' p @
  60.702 -          [str ")"])) ps, gr2)
  60.703 -      end
  60.704 -
  60.705 -    | _ => NONE)
  60.706 -  end;
  60.707 -
  60.708 -fun default_tycodegen thy mode defs dep module brack (TVar ((s, i), _)) gr =
  60.709 -      SOME (str (s ^ (if i = 0 then "" else string_of_int i)), gr)
  60.710 -  | default_tycodegen thy mode defs dep module brack (TFree (s, _)) gr =
  60.711 -      SOME (str s, gr)
  60.712 -  | default_tycodegen thy mode defs dep module brack (Type (s, Ts)) gr =
  60.713 -      (case AList.lookup (op =) ((#types o CodegenData.get) thy) s of
  60.714 -         NONE => NONE
  60.715 -       | SOME (ms, aux) =>
  60.716 -           let
  60.717 -             val (ps, gr') = fold_map
  60.718 -               (invoke_tycodegen thy mode defs dep module false)
  60.719 -               (fst (args_of ms Ts)) gr;
  60.720 -             val (qs, gr'') = fold_map
  60.721 -               (invoke_tycodegen thy mode defs dep module false)
  60.722 -               (quotes_of ms) gr';
  60.723 -             val module' = if_library mode (thyname_of_type thy s) module;
  60.724 -             val node_id = s ^ " (type)";
  60.725 -             fun p module' = Pretty.block (pretty_mixfix module module' ms ps qs)
  60.726 -           in SOME (case try (get_node gr'') node_id of
  60.727 -               NONE => (case get_aux_code mode aux of
  60.728 -                   [] => (p module', gr'')
  60.729 -                 | xs => (p module', snd (mk_type_id module' s
  60.730 -                       (add_edge (node_id, dep) (new_node (node_id,
  60.731 -                         (NONE, module', cat_lines xs ^ "\n")) gr'')))))
  60.732 -             | SOME (_, module'', _) =>
  60.733 -                 (p module'', add_edge (node_id, dep) gr''))
  60.734 -           end);
  60.735 -
  60.736 -fun mk_tuple [p] = p
  60.737 -  | mk_tuple ps = Pretty.block (str "(" ::
  60.738 -      flat (separate [str ",", Pretty.brk 1] (map single ps)) @ [str ")"]);
  60.739 -
  60.740 -fun mk_let bindings body =
  60.741 -  Pretty.blk (0, [str "let", Pretty.brk 1,
  60.742 -    Pretty.blk (0, separate Pretty.fbrk (map (fn (pat, rhs) =>
  60.743 -      Pretty.block [str "val ", pat, str " =", Pretty.brk 1,
  60.744 -      rhs, str ";"]) bindings)),
  60.745 -    Pretty.brk 1, str "in", Pretty.brk 1, body,
  60.746 -    Pretty.brk 1, str "end"]);
  60.747 -
  60.748 -fun mk_struct name s = "structure " ^ name ^ " =\nstruct\n\n" ^ s ^ "end;\n";
  60.749 -
  60.750 -fun add_to_module name s = AList.map_entry (op =) (name : string) (suffix s);
  60.751 -
  60.752 -fun output_code gr module xs =
  60.753 -  let
  60.754 -    val code = map_filter (fn s =>
  60.755 -      let val c as (_, module', _) = Graph.get_node gr s
  60.756 -      in if module = "" orelse module = module' then SOME (s, c) else NONE end)
  60.757 -        (rev (Graph.all_preds gr xs));
  60.758 -    fun string_of_cycle (a :: b :: cs) =
  60.759 -          let val SOME (x, y) = get_first (fn (x, (_, a', _)) =>
  60.760 -            if a = a' then Option.map (pair x)
  60.761 -              (find_first ((fn (_, b', _) => b' = b) o Graph.get_node gr)
  60.762 -                (Graph.imm_succs gr x))
  60.763 -            else NONE) code
  60.764 -          in x ^ " called by " ^ y ^ "\n" ^ string_of_cycle (b :: cs) end
  60.765 -      | string_of_cycle _ = ""
  60.766 -  in
  60.767 -    if module = "" then
  60.768 -      let
  60.769 -        val modules = distinct (op =) (map (#2 o snd) code);
  60.770 -        val mod_gr = fold_rev Graph.add_edge_acyclic
  60.771 -          (maps (fn (s, (_, module, _)) => map (pair module)
  60.772 -            (filter_out (fn s => s = module) (map (#2 o Graph.get_node gr)
  60.773 -              (Graph.imm_succs gr s)))) code)
  60.774 -          (fold_rev (Graph.new_node o rpair ()) modules Graph.empty);
  60.775 -        val modules' =
  60.776 -          rev (Graph.all_preds mod_gr (map (#2 o Graph.get_node gr) xs))
  60.777 -      in
  60.778 -        List.foldl (fn ((_, (_, module, s)), ms) => add_to_module module s ms)
  60.779 -          (map (rpair "") modules') code
  60.780 -      end handle Graph.CYCLES (cs :: _) =>
  60.781 -        error ("Cyclic dependency of modules:\n" ^ commas cs ^
  60.782 -          "\n" ^ string_of_cycle cs)
  60.783 -    else [(module, implode (map (#3 o snd) code))]
  60.784 -  end;
  60.785 -
  60.786 -fun gen_generate_code prep_term thy mode modules module xs =
  60.787 -  let
  60.788 -    val _ = (module <> "" orelse
  60.789 -        member (op =) mode "library" andalso forall (fn (s, _) => s = "") xs)
  60.790 -      orelse error "missing module name";
  60.791 -    val graphs = get_modules thy;
  60.792 -    val defs = mk_deftab thy;
  60.793 -    val gr = new_node ("<Top>", (NONE, module, ""))
  60.794 -      (List.foldl (fn ((gr, (tab1, tab2)), (gr', (tab1', tab2'))) =>
  60.795 -        (Graph.merge (fn ((_, module, _), (_, module', _)) =>
  60.796 -           module = module') (gr, gr'),
  60.797 -         (merge_nametabs (tab1, tab1'), merge_nametabs (tab2, tab2')))) emptygr
  60.798 -           (map (fn s => case Symtab.lookup graphs s of
  60.799 -                NONE => error ("Undefined code module: " ^ s)
  60.800 -              | SOME gr => gr) modules))
  60.801 -      handle Graph.DUP k => error ("Duplicate code for " ^ k);
  60.802 -    fun expand (t as Abs _) = t
  60.803 -      | expand t = (case fastype_of t of
  60.804 -          Type ("fun", [T, U]) => Abs ("x", T, t $ Bound 0) | _ => t);
  60.805 -    val (ps, gr') = fold_map (fn (s, t) => fn gr => apfst (pair s)
  60.806 -      (invoke_codegen thy mode defs "<Top>" module false t gr))
  60.807 -        (map (apsnd (expand o preprocess_term thy o prep_term thy)) xs) gr;
  60.808 -    val code = map_filter
  60.809 -      (fn ("", _) => NONE
  60.810 -        | (s', p) => SOME (string_of (Pretty.block
  60.811 -          [str ("val " ^ s' ^ " ="), Pretty.brk 1, p, str ";"]))) ps;
  60.812 -    val code' = space_implode "\n\n" code ^ "\n\n";
  60.813 -    val code'' =
  60.814 -      map_filter (fn (name, s) =>
  60.815 -          if member (op =) mode "library" andalso name = module andalso null code
  60.816 -          then NONE
  60.817 -          else SOME (name, mk_struct name s))
  60.818 -        ((if null code then I
  60.819 -          else add_to_module module code')
  60.820 -           (output_code (fst gr') (if_library mode "" module) ["<Top>"]))
  60.821 -  in
  60.822 -    (code'', del_nodes ["<Top>"] gr')
  60.823 -  end;
  60.824 -
  60.825 -val generate_code_i = gen_generate_code Sign.cert_term;
  60.826 -val generate_code =
  60.827 -  gen_generate_code (Syntax.read_term o Proof_Context.allow_dummies o Proof_Context.init_global);
  60.828 -
  60.829 -
  60.830 -(**** Reflection ****)
  60.831 -
  60.832 -val strip_tname = implode o tl o raw_explode;
  60.833 -
  60.834 -fun pretty_list xs = Pretty.block (str "[" ::
  60.835 -  flat (separate [str ",", Pretty.brk 1] (map single xs)) @
  60.836 -  [str "]"]);
  60.837 -
  60.838 -fun mk_type p (TVar ((s, i), _)) = str
  60.839 -      (strip_tname s ^ (if i = 0 then "" else string_of_int i) ^ "T")
  60.840 -  | mk_type p (TFree (s, _)) = str (strip_tname s ^ "T")
  60.841 -  | mk_type p (Type (s, Ts)) = (if p then parens else I) (Pretty.block
  60.842 -      [str "Type", Pretty.brk 1, str ("(\"" ^ s ^ "\","),
  60.843 -       Pretty.brk 1, pretty_list (map (mk_type false) Ts), str ")"]);
  60.844 -
  60.845 -fun mk_term_of gr module p (TVar ((s, i), _)) = str
  60.846 -      (strip_tname s ^ (if i = 0 then "" else string_of_int i) ^ "F")
  60.847 -  | mk_term_of gr module p (TFree (s, _)) = str (strip_tname s ^ "F")
  60.848 -  | mk_term_of gr module p (Type (s, Ts)) = (if p then parens else I)
  60.849 -      (Pretty.block (separate (Pretty.brk 1)
  60.850 -        (str (mk_qual_id module
  60.851 -          (get_type_id' (fn s' => "term_of_" ^ s') gr s)) ::
  60.852 -        maps (fn T =>
  60.853 -          [mk_term_of gr module true T, mk_type true T]) Ts)));
  60.854 -
  60.855 -
  60.856 -(**** Implicit results ****)
  60.857 -
  60.858 -structure Result = Proof_Data
  60.859 -(
  60.860 -  type T = (int -> term list option) * (unit -> term);
  60.861 -  fun init _ = (fn _ => NONE, fn () => Bound 0);
  60.862 -);
  60.863 -
  60.864 -val get_test_fn = #1 o Result.get;
  60.865 -val get_eval_fn = #2 o Result.get;
  60.866 -
  60.867 -fun poke_test_fn f = Context.>> (Context.map_proof (Result.map (fn (_, g) => (f, g))));
  60.868 -fun poke_eval_fn g = Context.>> (Context.map_proof (Result.map (fn (f, _) => (f, g))));
  60.869 -
  60.870 -
  60.871 -(**** Test data generators ****)
  60.872 -
  60.873 -fun mk_gen gr module p xs a (TVar ((s, i), _)) = str
  60.874 -      (strip_tname s ^ (if i = 0 then "" else string_of_int i) ^ "G")
  60.875 -  | mk_gen gr module p xs a (TFree (s, _)) = str (strip_tname s ^ "G")
  60.876 -  | mk_gen gr module p xs a (Type (tyc as (s, Ts))) = (if p then parens else I)
  60.877 -      (Pretty.block (separate (Pretty.brk 1)
  60.878 -        (str (mk_qual_id module (get_type_id' (fn s' => "gen_" ^ s') gr s) ^
  60.879 -          (if member (op =) xs s then "'" else "")) ::
  60.880 -         (case tyc of
  60.881 -            ("fun", [T, U]) =>
  60.882 -              [mk_term_of gr module true T, mk_type true T,
  60.883 -               mk_gen gr module true xs a U, mk_type true U]
  60.884 -          | _ => maps (fn T =>
  60.885 -              [mk_gen gr module true xs a T, mk_type true T]) Ts) @
  60.886 -         (if member (op =) xs s then [str a] else []))));
  60.887 -
  60.888 -fun test_term ctxt t =
  60.889 -  let
  60.890 -    val thy = Proof_Context.theory_of ctxt;
  60.891 -    val (code, gr) = generate_code_i thy ["term_of", "test"] [] "Generated" [("testf", t)];
  60.892 -    val Ts = map snd (fst (strip_abs t));
  60.893 -    val args = map_index (fn (i, T) => ("arg" ^ string_of_int i, T)) Ts;
  60.894 -    val s = "structure Test_Term =\nstruct\n\n" ^
  60.895 -      cat_lines (map snd code) ^
  60.896 -      "\nopen Generated;\n\n" ^ string_of
  60.897 -        (Pretty.block [str "val () = Codegen.poke_test_fn",
  60.898 -          Pretty.brk 1, str ("(fn i =>"), Pretty.brk 1,
  60.899 -          mk_let (map (fn (s, T) =>
  60.900 -              (mk_tuple [str s, str (s ^ "_t")],
  60.901 -               Pretty.block [mk_gen gr "Generated" false [] "" T, Pretty.brk 1,
  60.902 -                 str "i"])) args)
  60.903 -            (Pretty.block [str "if ",
  60.904 -              mk_app false (str "testf") (map (str o fst) args),
  60.905 -              Pretty.brk 1, str "then NONE",
  60.906 -              Pretty.brk 1, str "else ",
  60.907 -              Pretty.block [str "SOME ",
  60.908 -                Pretty.enum "," "[" "]" (map (fn (s, _) => str (s ^ "_t ()")) args)]]),
  60.909 -          str ");"]) ^
  60.910 -      "\n\nend;\n";
  60.911 -  in
  60.912 -    ctxt
  60.913 -    |> Context.proof_map (ML_Context.exec (fn () => ML_Context.eval_text false Position.none s))
  60.914 -    |> get_test_fn
  60.915 -  end;
  60.916 -
  60.917 -
  60.918 -(**** Evaluator for terms ****)
  60.919 -
  60.920 -fun eval_term ctxt t =
  60.921 -  let
  60.922 -    val _ =
  60.923 -      legacy_feature
  60.924 -        "Old evaluation mechanism -- use evaluator \"code\" or method \"eval\" instead";
  60.925 -    val thy = Proof_Context.theory_of ctxt;
  60.926 -    val _ = (null (Term.add_tvars t []) andalso null (Term.add_tfrees t [])) orelse
  60.927 -      error "Term to be evaluated contains type variables";
  60.928 -    val _ = (null (Term.add_vars t []) andalso null (Term.add_frees t [])) orelse
  60.929 -      error "Term to be evaluated contains variables";
  60.930 -    val (code, gr) =
  60.931 -      generate_code_i thy ["term_of"] [] "Generated"
  60.932 -        [("result", Abs ("x", TFree ("'a", []), t))];
  60.933 -    val s = "structure Eval_Term =\nstruct\n\n" ^
  60.934 -      cat_lines (map snd code) ^
  60.935 -      "\nopen Generated;\n\n" ^ string_of
  60.936 -        (Pretty.block [str "val () = Codegen.poke_eval_fn (fn () =>",
  60.937 -          Pretty.brk 1,
  60.938 -          mk_app false (mk_term_of gr "Generated" false (fastype_of t))
  60.939 -            [str "(result ())"],
  60.940 -          str ");"]) ^
  60.941 -      "\n\nend;\n";
  60.942 -    val eval_fn =
  60.943 -      ctxt
  60.944 -      |> Context.proof_map (ML_Context.exec (fn () => ML_Context.eval_text false Position.none s))
  60.945 -      |> get_eval_fn;
  60.946 -  in eval_fn () end;
  60.947 -
  60.948 -val (_, evaluation_oracle) = Context.>>> (Context.map_theory_result
  60.949 -  (Thm.add_oracle (Binding.name "evaluation", fn (ctxt, ct) =>
  60.950 -    let
  60.951 -      val thy = Proof_Context.theory_of ctxt;
  60.952 -      val t = Thm.term_of ct;
  60.953 -    in
  60.954 -      if Theory.subthy (Thm.theory_of_cterm ct, thy) then
  60.955 -        Thm.cterm_of thy (Logic.mk_equals (t, eval_term ctxt t))
  60.956 -      else raise CTERM ("evaluation_oracle: bad theory", [ct])
  60.957 -    end)));
  60.958 -
  60.959 -fun evaluation_conv ctxt ct = evaluation_oracle (ctxt, ct);
  60.960 -
  60.961 -
  60.962 -(**** Interface ****)
  60.963 -
  60.964 -fun parse_mixfix rd s =
  60.965 -  (case Scan.finite Symbol.stopper (Scan.repeat
  60.966 -     (   $$ "_" >> K Arg
  60.967 -      || $$ "?" >> K Ignore
  60.968 -      || $$ "\\<module>" >> K Module
  60.969 -      || $$ "/" |-- Scan.repeat ($$ " ") >> (Pretty o Pretty.brk o length)
  60.970 -      || $$ "{" |-- $$ "*" |-- Scan.repeat1
  60.971 -           (   $$ "'" |-- Scan.one Symbol.is_regular
  60.972 -            || Scan.unless ($$ "*" -- $$ "}") (Scan.one Symbol.is_regular)) --|
  60.973 -         $$ "*" --| $$ "}" >> (Quote o rd o implode)
  60.974 -      || Scan.repeat1
  60.975 -           (   $$ "'" |-- Scan.one Symbol.is_regular
  60.976 -            || Scan.unless ($$ "_" || $$ "?" || $$ "\\<module>" || $$ "/" || $$ "{" |-- $$ "*")
  60.977 -                 (Scan.one Symbol.is_regular)) >> (Pretty o str o implode)))
  60.978 -       (Symbol.explode s) of
  60.979 -     (p, []) => p
  60.980 -   | _ => error ("Malformed annotation: " ^ quote s));
  60.981 -
  60.982 -
  60.983 -val _ = List.app Keyword.keyword ["attach", "file", "contains"];
  60.984 -
  60.985 -fun strip_whitespace s = implode (fst (take_suffix (fn c => c = "\n" orelse c = " ")
  60.986 -  (snd (take_prefix (fn c => c = "\n" orelse c = " ") (raw_explode s))))) ^ "\n";
  60.987 -
  60.988 -val parse_attach = Scan.repeat (Parse.$$$ "attach" |--
  60.989 -  Scan.optional (Parse.$$$ "(" |-- Parse.xname --| Parse.$$$ ")") "" --
  60.990 -    (Parse.verbatim >> strip_whitespace));
  60.991 -
  60.992 -val _ =
  60.993 -  Outer_Syntax.command "types_code"
  60.994 -  "associate types with target language types" Keyword.thy_decl
  60.995 -    (Scan.repeat1 (Parse.xname --| Parse.$$$ "(" -- Parse.string --| Parse.$$$ ")" -- parse_attach) >>
  60.996 -     (fn xs => Toplevel.theory (fn thy => fold (assoc_type o
  60.997 -       (fn ((name, mfx), aux) => (name, (parse_mixfix
  60.998 -         (Syntax.read_typ_global thy) mfx, aux)))) xs thy)));
  60.999 -
 60.1000 -val _ =
 60.1001 -  Outer_Syntax.command "consts_code"
 60.1002 -  "associate constants with target language code" Keyword.thy_decl
 60.1003 -    (Scan.repeat1
 60.1004 -       (Parse.term --|
 60.1005 -        Parse.$$$ "(" -- Parse.string --| Parse.$$$ ")" -- parse_attach) >>
 60.1006 -     (fn xs => Toplevel.theory (fn thy => fold (assoc_const o
 60.1007 -       (fn ((const, mfx), aux) =>
 60.1008 -         (const, (parse_mixfix (Syntax.read_term_global thy) mfx, aux)))) xs thy)));
 60.1009 -
 60.1010 -fun parse_code lib =
 60.1011 -  Scan.optional (Parse.$$$ "(" |-- Parse.enum "," Parse.xname --| Parse.$$$ ")") [] --
 60.1012 -  (if lib then Scan.optional Parse.name "" else Parse.name) --
 60.1013 -  Scan.option (Parse.$$$ "file" |-- Parse.name) --
 60.1014 -  (if lib then Scan.succeed []
 60.1015 -   else Scan.optional (Parse.$$$ "imports" |-- Scan.repeat1 Parse.name) []) --|
 60.1016 -  Parse.$$$ "contains" --
 60.1017 -  (   Scan.repeat1 (Parse.name --| Parse.$$$ "=" -- Parse.term)
 60.1018 -   || Scan.repeat1 (Parse.term >> pair "")) >>
 60.1019 -  (fn ((((mode, module), opt_fname), modules), xs) => Toplevel.theory (fn thy =>
 60.1020 -    let
 60.1021 -      val _ = legacy_feature "Old code generation command -- use 'export_code' instead";
 60.1022 -      val mode' = (if lib then insert (op =) "library" else I) (remove (op =) "library" mode);
 60.1023 -      val (code, gr) = generate_code thy mode' modules module xs;
 60.1024 -      val thy' = thy |> Context.theory_map (ML_Context.exec (fn () =>
 60.1025 -        (case opt_fname of
 60.1026 -          NONE => ML_Context.eval_text false Position.none (cat_lines (map snd code))
 60.1027 -        | SOME fname =>
 60.1028 -            if lib then app (fn (name, s) => File.write
 60.1029 -                (Path.append (Path.explode fname) (Path.basic (name ^ ".ML"))) s)
 60.1030 -              (("ROOT", implode (map (fn (name, _) =>
 60.1031 -                  "use \"" ^ name ^ ".ML\";\n") code)) :: code)
 60.1032 -            else File.write (Path.explode fname) (snd (hd code)))));
 60.1033 -    in
 60.1034 -      if lib then thy'
 60.1035 -      else map_modules (Symtab.update (module, gr)) thy'
 60.1036 -    end));
 60.1037 -
 60.1038 -val setup = add_codegen "default" default_codegen
 60.1039 -  #> add_tycodegen "default" default_tycodegen
 60.1040 -  #> add_preprocessor unfold_preprocessor;
 60.1041 -
 60.1042 -val _ =
 60.1043 -  Outer_Syntax.command "code_library"
 60.1044 -    "generate code for terms (one structure for each theory)" Keyword.thy_decl
 60.1045 -    (parse_code true);
 60.1046 -
 60.1047 -val _ =
 60.1048 -  Outer_Syntax.command "code_module"
 60.1049 -    "generate code for terms (single structure, incremental)" Keyword.thy_decl
 60.1050 -    (parse_code false);
 60.1051 -
 60.1052 -end;
    61.1 --- a/src/Pure/drule.ML	Wed Aug 10 18:02:16 2011 -0700
    61.2 +++ b/src/Pure/drule.ML	Wed Aug 10 18:07:32 2011 -0700
    61.3 @@ -302,20 +302,18 @@
    61.4  
    61.5  
    61.6  (*Convert all Vars in a theorem to Frees.  Also return a function for
    61.7 -  reversing that operation.  DOES NOT WORK FOR TYPE VARIABLES.
    61.8 -  Similar code in type/freeze_thaw*)
    61.9 +  reversing that operation.  DOES NOT WORK FOR TYPE VARIABLES.*)
   61.10  
   61.11  fun legacy_freeze_thaw_robust th =
   61.12   let val fth = Thm.legacy_freezeT th
   61.13       val thy = Thm.theory_of_thm fth
   61.14 -     val {prop, tpairs, ...} = rep_thm fth
   61.15   in
   61.16 -   case List.foldr OldTerm.add_term_vars [] (prop :: Thm.terms_of_tpairs tpairs) of
   61.17 +   case Thm.fold_terms Term.add_vars fth [] of
   61.18         [] => (fth, fn i => fn x => x)   (*No vars: nothing to do!*)
   61.19       | vars =>
   61.20 -         let fun newName (Var(ix,_)) = (ix, legacy_gensym (string_of_indexname ix))
   61.21 +         let fun newName (ix,_) = (ix, legacy_gensym (string_of_indexname ix))
   61.22               val alist = map newName vars
   61.23 -             fun mk_inst (Var(v,T)) =
   61.24 +             fun mk_inst (v,T) =
   61.25                   (cterm_of thy (Var(v,T)),
   61.26                    cterm_of thy (Free(((the o AList.lookup (op =) alist) v), T)))
   61.27               val insts = map mk_inst vars
   61.28 @@ -330,17 +328,16 @@
   61.29  fun legacy_freeze_thaw th =
   61.30   let val fth = Thm.legacy_freezeT th
   61.31       val thy = Thm.theory_of_thm fth
   61.32 -     val {prop, tpairs, ...} = rep_thm fth
   61.33   in
   61.34 -   case List.foldr OldTerm.add_term_vars [] (prop :: Thm.terms_of_tpairs tpairs) of
   61.35 +   case Thm.fold_terms Term.add_vars fth [] of
   61.36         [] => (fth, fn x => x)
   61.37       | vars =>
   61.38 -         let fun newName (Var(ix,_), (pairs,used)) =
   61.39 +         let fun newName (ix, _) (pairs, used) =
   61.40                     let val v = singleton (Name.variant_list used) (string_of_indexname ix)
   61.41                     in  ((ix,v)::pairs, v::used)  end;
   61.42 -             val (alist, _) = List.foldr newName ([], Library.foldr OldTerm.add_term_names
   61.43 -               (prop :: Thm.terms_of_tpairs tpairs, [])) vars
   61.44 -             fun mk_inst (Var(v,T)) =
   61.45 +             val (alist, _) =
   61.46 +                 fold_rev newName vars ([], Thm.fold_terms Term.add_free_names fth [])
   61.47 +             fun mk_inst (v, T) =
   61.48                   (cterm_of thy (Var(v,T)),
   61.49                    cterm_of thy (Free(((the o AList.lookup (op =) alist) v), T)))
   61.50               val insts = map mk_inst vars
    62.1 --- a/src/Pure/goal.ML	Wed Aug 10 18:02:16 2011 -0700
    62.2 +++ b/src/Pure/goal.ML	Wed Aug 10 18:07:32 2011 -0700
    62.3 @@ -124,12 +124,11 @@
    62.4      let
    62.5        val _ = forked 1;
    62.6        val future =
    62.7 -        singleton (Future.forks {name = name, group = NONE, deps = [], pri = ~1})
    62.8 +        singleton
    62.9 +          (Future.forks {name = name, group = NONE, deps = [], pri = ~1, interrupts = false})
   62.10            (fn () =>
   62.11 -            (*interruptible*)
   62.12              Exn.release
   62.13 -              (Exn.capture Future.status e before forked ~1
   62.14 -                handle exn => (forked ~1; reraise exn)));
   62.15 +              (Exn.capture (Future.status o Future.interruptible_task) e before forked ~1));
   62.16      in future end) ();
   62.17  
   62.18  fun fork e = fork_name "Goal.fork" e;
    63.1 --- a/src/Pure/old_term.ML	Wed Aug 10 18:02:16 2011 -0700
    63.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    63.3 @@ -1,94 +0,0 @@
    63.4 -(*  Title:      Pure/old_term.ML
    63.5 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    63.6 -
    63.7 -Some outdated term operations.
    63.8 -*)
    63.9 -
   63.10 -signature OLD_TERM =
   63.11 -sig
   63.12 -  val it_term_types: (typ * 'a -> 'a) -> term * 'a -> 'a
   63.13 -  val add_term_names: term * string list -> string list
   63.14 -  val add_typ_tvars: typ * (indexname * sort) list -> (indexname * sort) list
   63.15 -  val add_typ_tfree_names: typ * string list -> string list
   63.16 -  val add_typ_tfrees: typ * (string * sort) list -> (string * sort) list
   63.17 -  val add_term_tvars: term * (indexname * sort) list -> (indexname * sort) list
   63.18 -  val add_term_tfrees: term * (string * sort) list -> (string * sort) list
   63.19 -  val add_term_tfree_names: term * string list -> string list
   63.20 -  val typ_tfrees: typ -> (string * sort) list
   63.21 -  val typ_tvars: typ -> (indexname * sort) list
   63.22 -  val term_tfrees: term -> (string * sort) list
   63.23 -  val term_tvars: term -> (indexname * sort) list
   63.24 -  val add_term_vars: term * term list -> term list
   63.25 -  val term_vars: term -> term list
   63.26 -  val add_term_frees: term * term list -> term list
   63.27 -  val term_frees: term -> term list
   63.28 -end;
   63.29 -
   63.30 -structure OldTerm: OLD_TERM =
   63.31 -struct
   63.32 -
   63.33 -(*iterate a function over all types in a term*)
   63.34 -fun it_term_types f =
   63.35 -let fun iter(Const(_,T), a) = f(T,a)
   63.36 -      | iter(Free(_,T), a) = f(T,a)
   63.37 -      | iter(Var(_,T), a) = f(T,a)
   63.38 -      | iter(Abs(_,T,t), a) = iter(t,f(T,a))
   63.39 -      | iter(f$u, a) = iter(f, iter(u, a))
   63.40 -      | iter(Bound _, a) = a
   63.41 -in iter end
   63.42 -
   63.43 -(*Accumulates the names in the term, suppressing duplicates.
   63.44 -  Includes Frees and Consts.  For choosing unambiguous bound var names.*)
   63.45 -fun add_term_names (Const(a,_), bs) = insert (op =) (Long_Name.base_name a) bs
   63.46 -  | add_term_names (Free(a,_), bs) = insert (op =) a bs
   63.47 -  | add_term_names (f$u, bs) = add_term_names (f, add_term_names(u, bs))
   63.48 -  | add_term_names (Abs(_,_,t), bs) = add_term_names(t,bs)
   63.49 -  | add_term_names (_, bs) = bs;
   63.50 -
   63.51 -(*Accumulates the TVars in a type, suppressing duplicates.*)
   63.52 -fun add_typ_tvars(Type(_,Ts),vs) = List.foldr add_typ_tvars vs Ts
   63.53 -  | add_typ_tvars(TFree(_),vs) = vs
   63.54 -  | add_typ_tvars(TVar(v),vs) = insert (op =) v vs;
   63.55 -
   63.56 -(*Accumulates the TFrees in a type, suppressing duplicates.*)
   63.57 -fun add_typ_tfree_names(Type(_,Ts),fs) = List.foldr add_typ_tfree_names fs Ts
   63.58 -  | add_typ_tfree_names(TFree(f,_),fs) = insert (op =) f fs
   63.59 -  | add_typ_tfree_names(TVar(_),fs) = fs;
   63.60 -
   63.61 -fun add_typ_tfrees(Type(_,Ts),fs) = List.foldr add_typ_tfrees fs Ts
   63.62 -  | add_typ_tfrees(TFree(f),fs) = insert (op =) f fs
   63.63 -  | add_typ_tfrees(TVar(_),fs) = fs;
   63.64 -
   63.65 -(*Accumulates the TVars in a term, suppressing duplicates.*)
   63.66 -val add_term_tvars = it_term_types add_typ_tvars;
   63.67 -
   63.68 -(*Accumulates the TFrees in a term, suppressing duplicates.*)
   63.69 -val add_term_tfrees = it_term_types add_typ_tfrees;
   63.70 -val add_term_tfree_names = it_term_types add_typ_tfree_names;
   63.71 -
   63.72 -(*Non-list versions*)
   63.73 -fun typ_tfrees T = add_typ_tfrees(T,[]);
   63.74 -fun typ_tvars T = add_typ_tvars(T,[]);
   63.75 -fun term_tfrees t = add_term_tfrees(t,[]);
   63.76 -fun term_tvars t = add_term_tvars(t,[]);
   63.77 -
   63.78 -
   63.79 -(*Accumulates the Vars in the term, suppressing duplicates.*)
   63.80 -fun add_term_vars (t, vars: term list) = case t of
   63.81 -    Var   _ => Ord_List.insert Term_Ord.term_ord t vars
   63.82 -  | Abs (_,_,body) => add_term_vars(body,vars)
   63.83 -  | f$t =>  add_term_vars (f, add_term_vars(t, vars))
   63.84 -  | _ => vars;
   63.85 -
   63.86 -fun term_vars t = add_term_vars(t,[]);
   63.87 -
   63.88 -(*Accumulates the Frees in the term, suppressing duplicates.*)
   63.89 -fun add_term_frees (t, frees: term list) = case t of
   63.90 -    Free   _ => Ord_List.insert Term_Ord.term_ord t frees
   63.91 -  | Abs (_,_,body) => add_term_frees(body,frees)
   63.92 -  | f$t =>  add_term_frees (f, add_term_frees(t, frees))
   63.93 -  | _ => frees;
   63.94 -
   63.95 -fun term_frees t = add_term_frees(t,[]);
   63.96 -
   63.97 -end;
    64.1 --- a/src/Pure/proofterm.ML	Wed Aug 10 18:02:16 2011 -0700
    64.2 +++ b/src/Pure/proofterm.ML	Wed Aug 10 18:07:32 2011 -0700
    64.3 @@ -461,15 +461,15 @@
    64.4  fun del_conflicting_tvars envT T = Term_Subst.instantiateT
    64.5    (map_filter (fn ixnS as (_, S) =>
    64.6       (Type.lookup envT ixnS; NONE) handle TYPE _ =>
    64.7 -        SOME (ixnS, TFree ("'dummy", S))) (OldTerm.typ_tvars T)) T;
    64.8 +        SOME (ixnS, TFree ("'dummy", S))) (Term.add_tvarsT T [])) T;
    64.9  
   64.10  fun del_conflicting_vars env t = Term_Subst.instantiate
   64.11    (map_filter (fn ixnS as (_, S) =>
   64.12       (Type.lookup (Envir.type_env env) ixnS; NONE) handle TYPE _ =>
   64.13 -        SOME (ixnS, TFree ("'dummy", S))) (OldTerm.term_tvars t),
   64.14 -   map_filter (fn Var (ixnT as (_, T)) =>
   64.15 +        SOME (ixnS, TFree ("'dummy", S))) (Term.add_tvars t []),
   64.16 +   map_filter (fn (ixnT as (_, T)) =>
   64.17       (Envir.lookup (env, ixnT); NONE) handle TYPE _ =>
   64.18 -        SOME (ixnT, Free ("dummy", T))) (OldTerm.term_vars t)) t;
   64.19 +        SOME (ixnT, Free ("dummy", T))) (Term.add_vars t [])) t;
   64.20  
   64.21  fun norm_proof env =
   64.22    let
   64.23 @@ -674,11 +674,12 @@
   64.24  
   64.25  local
   64.26  
   64.27 -fun new_name (ix, (pairs,used)) =
   64.28 +fun new_name ix (pairs, used) =
   64.29    let val v = singleton (Name.variant_list used) (string_of_indexname ix)
   64.30 -  in  ((ix, v) :: pairs, v :: used)  end;
   64.31 +  in ((ix, v) :: pairs, v :: used) end;
   64.32  
   64.33 -fun freeze_one alist (ix, sort) = (case AList.lookup (op =) alist ix of
   64.34 +fun freeze_one alist (ix, sort) =
   64.35 +  (case AList.lookup (op =) alist ix of
   64.36      NONE => TVar (ix, sort)
   64.37    | SOME name => TFree (name, sort));
   64.38  
   64.39 @@ -686,15 +687,14 @@
   64.40  
   64.41  fun legacy_freezeT t prf =
   64.42    let
   64.43 -    val used = OldTerm.it_term_types OldTerm.add_typ_tfree_names (t, [])
   64.44 -    and tvars = map #1 (OldTerm.it_term_types OldTerm.add_typ_tvars (t, []));
   64.45 -    val (alist, _) = List.foldr new_name ([], used) tvars;
   64.46 +    val used = Term.add_tfree_names t [];
   64.47 +    val (alist, _) = fold_rev new_name (map #1 (Term.add_tvars t [])) ([], used);
   64.48    in
   64.49      (case alist of
   64.50        [] => prf (*nothing to do!*)
   64.51      | _ =>
   64.52 -      let val frzT = map_type_tvar (freeze_one alist)
   64.53 -      in map_proof_terms (map_types frzT) frzT prf end)
   64.54 +        let val frzT = map_type_tvar (freeze_one alist)
   64.55 +        in map_proof_terms (map_types frzT) frzT prf end)
   64.56    end;
   64.57  
   64.58  end;
   64.59 @@ -1404,7 +1404,8 @@
   64.60    | fulfill_proof_future thy promises postproc body =
   64.61        singleton
   64.62          (Future.forks {name = "Proofterm.fulfill_proof_future", group = NONE,
   64.63 -            deps = Future.task_of body :: map (Future.task_of o snd) promises, pri = 0})
   64.64 +            deps = Future.task_of body :: map (Future.task_of o snd) promises, pri = 0,
   64.65 +            interrupts = true})
   64.66          (fn () =>
   64.67            postproc (fulfill_norm_proof thy (map (apsnd Future.join) promises) (Future.join body)));
   64.68  
   64.69 @@ -1461,7 +1462,9 @@
   64.70        else if not (Multithreading.enabled ()) then Future.value (make_body0 (full_proof0 ()))
   64.71        else
   64.72          singleton
   64.73 -          (Future.forks {name = "Proofterm.prepare_thm_proof", group = NONE, deps = [], pri = ~1})
   64.74 +          (Future.forks
   64.75 +            {name = "Proofterm.prepare_thm_proof", group = NONE, deps = [], pri = ~1,
   64.76 +              interrupts = true})
   64.77            (make_body0 o full_proof0);
   64.78  
   64.79      fun new_prf () = (serial (), fulfill_proof_future thy promises postproc body0);
    65.1 --- a/src/Pure/type.ML	Wed Aug 10 18:02:16 2011 -0700
    65.2 +++ b/src/Pure/type.ML	Wed Aug 10 18:07:32 2011 -0700
    65.3 @@ -358,7 +358,7 @@
    65.4  
    65.5  local
    65.6  
    65.7 -fun new_name (ix, (pairs, used)) =
    65.8 +fun new_name ix (pairs, used) =
    65.9    let val v = singleton (Name.variant_list used) (string_of_indexname ix)
   65.10    in ((ix, v) :: pairs, v :: used) end;
   65.11  
   65.12 @@ -374,18 +374,16 @@
   65.13  
   65.14  fun legacy_freeze_thaw_type T =
   65.15    let
   65.16 -    val used = OldTerm.add_typ_tfree_names (T, [])
   65.17 -    and tvars = map #1 (OldTerm.add_typ_tvars (T, []));
   65.18 -    val (alist, _) = List.foldr new_name ([], used) tvars;
   65.19 +    val used = Term.add_tfree_namesT T [];
   65.20 +    val (alist, _) = fold_rev new_name (map #1 (Term.add_tvarsT T [])) ([], used);
   65.21    in (map_type_tvar (freeze_one alist) T, map_type_tfree (thaw_one (map swap alist))) end;
   65.22  
   65.23  val legacy_freeze_type = #1 o legacy_freeze_thaw_type;
   65.24  
   65.25  fun legacy_freeze_thaw t =
   65.26    let
   65.27 -    val used = OldTerm.it_term_types OldTerm.add_typ_tfree_names (t, [])
   65.28 -    and tvars = map #1 (OldTerm.it_term_types OldTerm.add_typ_tvars (t, []));
   65.29 -    val (alist, _) = List.foldr new_name ([], used) tvars;
   65.30 +    val used = Term.add_tfree_names t [];
   65.31 +    val (alist, _) = fold_rev new_name (map #1 (Term.add_tvars t [])) ([], used);
   65.32    in
   65.33      (case alist of
   65.34        [] => (t, fn x => x) (*nothing to do!*)
    66.1 --- a/src/Tools/Code_Generator.thy	Wed Aug 10 18:02:16 2011 -0700
    66.2 +++ b/src/Tools/Code_Generator.thy	Wed Aug 10 18:07:32 2011 -0700
    66.3 @@ -7,6 +7,8 @@
    66.4  theory Code_Generator
    66.5  imports Pure
    66.6  uses
    66.7 +  "~~/src/Tools/misc_legacy.ML"
    66.8 +  "~~/src/Tools/codegen.ML"
    66.9    "~~/src/Tools/cache_io.ML"
   66.10    "~~/src/Tools/try.ML"
   66.11    "~~/src/Tools/solve_direct.ML"
    67.1 --- a/src/Tools/IsaPlanner/isand.ML	Wed Aug 10 18:02:16 2011 -0700
    67.2 +++ b/src/Tools/IsaPlanner/isand.ML	Wed Aug 10 18:07:32 2011 -0700
    67.3 @@ -186,8 +186,8 @@
    67.4  (* change type-vars to fresh type frees *)
    67.5  fun fix_tvars_to_tfrees_in_terms names ts = 
    67.6      let 
    67.7 -      val tfree_names = map fst (List.foldr OldTerm.add_term_tfrees [] ts);
    67.8 -      val tvars = List.foldr OldTerm.add_term_tvars [] ts;
    67.9 +      val tfree_names = map fst (List.foldr Misc_Legacy.add_term_tfrees [] ts);
   67.10 +      val tvars = List.foldr Misc_Legacy.add_term_tvars [] ts;
   67.11        val (names',renamings) = 
   67.12            List.foldr (fn (tv as ((n,i),s),(Ns,Rs)) => 
   67.13                           let val n2 = singleton (Name.variant_list Ns) n in 
   67.14 @@ -212,15 +212,15 @@
   67.15  fun unfix_tfrees ns th = 
   67.16      let 
   67.17        val varfiytfrees = map (Term.dest_TFree o Thm.typ_of) ns
   67.18 -      val skiptfrees = subtract (op =) varfiytfrees (OldTerm.add_term_tfrees (Thm.prop_of th,[]));
   67.19 +      val skiptfrees = subtract (op =) varfiytfrees (Misc_Legacy.add_term_tfrees (Thm.prop_of th,[]));
   67.20      in #2 (Thm.varifyT_global' skiptfrees th) end;
   67.21  
   67.22  (* change schematic/meta vars to fresh free vars, avoiding name clashes 
   67.23     with "names" *)
   67.24  fun fix_vars_to_frees_in_terms names ts = 
   67.25      let 
   67.26 -      val vars = map Term.dest_Var (List.foldr OldTerm.add_term_vars [] ts);
   67.27 -      val Ns = List.foldr OldTerm.add_term_names names ts;
   67.28 +      val vars = map Term.dest_Var (List.foldr Misc_Legacy.add_term_vars [] ts);
   67.29 +      val Ns = List.foldr Misc_Legacy.add_term_names names ts;
   67.30        val (_,renamings) = 
   67.31            Library.foldl (fn ((Ns,Rs),v as ((n,i),ty)) => 
   67.32                      let val n2 = singleton (Name.variant_list Ns) n in
   67.33 @@ -245,7 +245,7 @@
   67.34        val ctypify = Thm.ctyp_of sgn
   67.35        val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th);
   67.36        val prop = (Thm.prop_of th);
   67.37 -      val tvars = List.foldr OldTerm.add_term_tvars [] (prop :: tpairs);
   67.38 +      val tvars = List.foldr Misc_Legacy.add_term_tvars [] (prop :: tpairs);
   67.39        val ctyfixes = 
   67.40            map_filter 
   67.41              (fn (v as ((s,i),ty)) => 
   67.42 @@ -258,7 +258,7 @@
   67.43        val ctermify = Thm.cterm_of sgn
   67.44        val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th);
   67.45        val prop = (Thm.prop_of th);
   67.46 -      val vars = map Term.dest_Var (List.foldr OldTerm.add_term_vars 
   67.47 +      val vars = map Term.dest_Var (List.foldr Misc_Legacy.add_term_vars 
   67.48                                                 [] (prop :: tpairs));
   67.49        val cfixes = 
   67.50            map_filter 
   67.51 @@ -359,7 +359,7 @@
   67.52        val sgn = Thm.theory_of_thm th;
   67.53        val ctermify = Thm.cterm_of sgn;
   67.54  
   67.55 -      val allfrees = map Term.dest_Free (OldTerm.term_frees (Thm.prop_of th))
   67.56 +      val allfrees = map Term.dest_Free (Misc_Legacy.term_frees (Thm.prop_of th))
   67.57        val cfrees = map (ctermify o Free o lookupfree allfrees) vs
   67.58  
   67.59        val sgs = prems_of th;
   67.60 @@ -419,8 +419,8 @@
   67.61      let
   67.62        val t = Term.strip_all_body alledt;
   67.63        val alls = rev (Term.strip_all_vars alledt);
   67.64 -      val varnames = map (fst o fst o Term.dest_Var) (OldTerm.term_vars t)
   67.65 -      val names = OldTerm.add_term_names (t,varnames);
   67.66 +      val varnames = map (fst o fst o Term.dest_Var) (Misc_Legacy.term_vars t)
   67.67 +      val names = Misc_Legacy.add_term_names (t,varnames);
   67.68        val fvs = map Free 
   67.69                      (Name.variant_list names (map fst alls)
   67.70                         ~~ (map snd alls));
   67.71 @@ -428,8 +428,8 @@
   67.72  
   67.73  fun fix_alls_term i t = 
   67.74      let 
   67.75 -      val varnames = map (fst o fst o Term.dest_Var) (OldTerm.term_vars t)
   67.76 -      val names = OldTerm.add_term_names (t,varnames);
   67.77 +      val varnames = map (fst o fst o Term.dest_Var) (Misc_Legacy.term_vars t)
   67.78 +      val names = Misc_Legacy.add_term_names (t,varnames);
   67.79        val gt = Logic.get_goal t i;
   67.80        val body = Term.strip_all_body gt;
   67.81        val alls = rev (Term.strip_all_vars gt);
    68.1 --- a/src/Tools/IsaPlanner/rw_inst.ML	Wed Aug 10 18:02:16 2011 -0700
    68.2 +++ b/src/Tools/IsaPlanner/rw_inst.ML	Wed Aug 10 18:07:32 2011 -0700
    68.3 @@ -71,7 +71,7 @@
    68.4        val (tpairl,tpairr) = Library.split_list (#tpairs rep)
    68.5        val prop = #prop rep
    68.6      in
    68.7 -      List.foldr OldTerm.add_term_names [] (prop :: (tpairl @ (tpairr @ hyps)))
    68.8 +      List.foldr Misc_Legacy.add_term_names [] (prop :: (tpairl @ (tpairr @ hyps)))
    68.9      end;
   68.10  
   68.11  (* Given a list of variables that were bound, and a that has been
   68.12 @@ -136,13 +136,13 @@
   68.13  fun mk_renamings tgt rule_inst = 
   68.14      let
   68.15        val rule_conds = Thm.prems_of rule_inst
   68.16 -      val names = List.foldr OldTerm.add_term_names [] (tgt :: rule_conds);
   68.17 +      val names = List.foldr Misc_Legacy.add_term_names [] (tgt :: rule_conds);
   68.18        val (conds_tyvs,cond_vs) = 
   68.19            Library.foldl (fn ((tyvs, vs), t) => 
   68.20 -                    (union (op =) (OldTerm.term_tvars t) tyvs,
   68.21 -                     union (op =) (map Term.dest_Var (OldTerm.term_vars t)) vs))
   68.22 +                    (union (op =) (Misc_Legacy.term_tvars t) tyvs,
   68.23 +                     union (op =) (map Term.dest_Var (Misc_Legacy.term_vars t)) vs))
   68.24                  (([],[]), rule_conds);
   68.25 -      val termvars = map Term.dest_Var (OldTerm.term_vars tgt); 
   68.26 +      val termvars = map Term.dest_Var (Misc_Legacy.term_vars tgt); 
   68.27        val vars_to_fix = union (op =) termvars cond_vs;
   68.28        val (renamings, names2) = 
   68.29            List.foldr (fn (((n,i),ty), (vs, names')) => 
   68.30 @@ -165,8 +165,8 @@
   68.31        val ignore_ixs = map fst ignore_insts;
   68.32        val (tvars, tfrees) = 
   68.33              List.foldr (fn (t, (varixs, tfrees)) => 
   68.34 -                      (OldTerm.add_term_tvars (t,varixs),
   68.35 -                       OldTerm.add_term_tfrees (t,tfrees)))
   68.36 +                      (Misc_Legacy.add_term_tvars (t,varixs),
   68.37 +                       Misc_Legacy.add_term_tfrees (t,tfrees)))
   68.38                    ([],[]) ts;
   68.39          val unfixed_tvars = 
   68.40              filter (fn (ix,s) => not (member (op =) ignore_ixs ix)) tvars;
    69.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    69.2 +++ b/src/Tools/codegen.ML	Wed Aug 10 18:07:32 2011 -0700
    69.3 @@ -0,0 +1,1049 @@
    69.4 +(*  Title:      Tools/codegen.ML
    69.5 +    Author:     Stefan Berghofer, TU Muenchen
    69.6 +
    69.7 +Old code generator.
    69.8 +*)
    69.9 +
   69.10 +signature CODEGEN =
   69.11 +sig
   69.12 +  val quiet_mode : bool Unsynchronized.ref
   69.13 +  val message : string -> unit
   69.14 +  val margin : int Unsynchronized.ref
   69.15 +  val string_of : Pretty.T -> string
   69.16 +  val str : string -> Pretty.T
   69.17 +
   69.18 +  datatype 'a mixfix =
   69.19 +      Arg
   69.20 +    | Ignore
   69.21 +    | Module
   69.22 +    | Pretty of Pretty.T
   69.23 +    | Quote of 'a;
   69.24 +
   69.25 +  type deftab
   69.26 +  type node
   69.27 +  type codegr
   69.28 +  type 'a codegen
   69.29 +
   69.30 +  val add_codegen: string -> term codegen -> theory -> theory
   69.31 +  val add_tycodegen: string -> typ codegen -> theory -> theory
   69.32 +  val add_preprocessor: (theory -> thm list -> thm list) -> theory -> theory
   69.33 +  val preprocess: theory -> thm list -> thm list
   69.34 +  val preprocess_term: theory -> term -> term
   69.35 +  val print_codegens: theory -> unit
   69.36 +  val generate_code: theory -> string list -> string list -> string -> (string * string) list ->
   69.37 +    (string * string) list * codegr
   69.38 +  val generate_code_i: theory -> string list -> string list -> string -> (string * term) list ->
   69.39 +    (string * string) list * codegr
   69.40 +  val assoc_const: string * (term mixfix list *
   69.41 +    (string * string) list) -> theory -> theory
   69.42 +  val assoc_const_i: (string * typ) * (term mixfix list *
   69.43 +    (string * string) list) -> theory -> theory
   69.44 +  val assoc_type: xstring * (typ mixfix list *
   69.45 +    (string * string) list) -> theory -> theory
   69.46 +  val get_assoc_code: theory -> string * typ ->
   69.47 +    (term mixfix list * (string * string) list) option
   69.48 +  val get_assoc_type: theory -> string ->
   69.49 +    (typ mixfix list * (string * string) list) option
   69.50 +  val codegen_error: codegr -> string -> string -> 'a
   69.51 +  val invoke_codegen: theory -> string list -> deftab -> string -> string -> bool ->
   69.52 +    term -> codegr -> Pretty.T * codegr
   69.53 +  val invoke_tycodegen: theory -> string list -> deftab -> string -> string -> bool ->
   69.54 +    typ -> codegr -> Pretty.T * codegr
   69.55 +  val mk_id: string -> string
   69.56 +  val mk_qual_id: string -> string * string -> string
   69.57 +  val mk_const_id: string -> string -> codegr -> (string * string) * codegr
   69.58 +  val get_const_id: codegr -> string -> string * string
   69.59 +  val mk_type_id: string -> string -> codegr -> (string * string) * codegr
   69.60 +  val get_type_id: codegr -> string -> string * string
   69.61 +  val thyname_of_type: theory -> string -> string
   69.62 +  val thyname_of_const: theory -> string -> string
   69.63 +  val rename_terms: term list -> term list
   69.64 +  val rename_term: term -> term
   69.65 +  val new_names: term -> string list -> string list
   69.66 +  val new_name: term -> string -> string
   69.67 +  val if_library: string list -> 'a -> 'a -> 'a
   69.68 +  val get_defn: theory -> deftab -> string -> typ ->
   69.69 +    ((typ * (string * thm)) * int option) option
   69.70 +  val is_instance: typ -> typ -> bool
   69.71 +  val parens: Pretty.T -> Pretty.T
   69.72 +  val mk_app: bool -> Pretty.T -> Pretty.T list -> Pretty.T
   69.73 +  val mk_tuple: Pretty.T list -> Pretty.T
   69.74 +  val mk_let: (Pretty.T * Pretty.T) list -> Pretty.T -> Pretty.T
   69.75 +  val eta_expand: term -> term list -> int -> term
   69.76 +  val strip_tname: string -> string
   69.77 +  val mk_type: bool -> typ -> Pretty.T
   69.78 +  val mk_term_of: codegr -> string -> bool -> typ -> Pretty.T
   69.79 +  val mk_gen: codegr -> string -> bool -> string list -> string -> typ -> Pretty.T
   69.80 +  val poke_test_fn: (int -> term list option) -> unit
   69.81 +  val poke_eval_fn: (unit -> term) -> unit
   69.82 +  val test_term: Proof.context -> term -> int -> term list option
   69.83 +  val eval_term: Proof.context -> term -> term
   69.84 +  val evaluation_conv: Proof.context -> conv
   69.85 +  val parse_mixfix: (string -> 'a) -> string -> 'a mixfix list
   69.86 +  val quotes_of: 'a mixfix list -> 'a list
   69.87 +  val num_args_of: 'a mixfix list -> int
   69.88 +  val replace_quotes: 'b list -> 'a mixfix list -> 'b mixfix list
   69.89 +  val mk_deftab: theory -> deftab
   69.90 +  val map_unfold: (simpset -> simpset) -> theory -> theory
   69.91 +  val add_unfold: thm -> theory -> theory
   69.92 +  val del_unfold: thm -> theory -> theory
   69.93 +
   69.94 +  val get_node: codegr -> string -> node
   69.95 +  val add_edge: string * string -> codegr -> codegr
   69.96 +  val add_edge_acyclic: string * string -> codegr -> codegr
   69.97 +  val del_nodes: string list -> codegr -> codegr
   69.98 +  val map_node: string -> (node -> node) -> codegr -> codegr
   69.99 +  val new_node: string * node -> codegr -> codegr
  69.100 +
  69.101 +  val setup: theory -> theory
  69.102 +end;
  69.103 +
  69.104 +structure Codegen : CODEGEN =
  69.105 +struct
  69.106 +
  69.107 +val quiet_mode = Unsynchronized.ref true;
  69.108 +fun message s = if !quiet_mode then () else writeln s;
  69.109 +
  69.110 +val margin = Unsynchronized.ref 80;
  69.111 +
  69.112 +fun string_of p = Print_Mode.setmp [] (Pretty.string_of_margin (!margin)) p;
  69.113 +
  69.114 +val str = Print_Mode.setmp [] Pretty.str;
  69.115 +
  69.116 +(**** Mixfix syntax ****)
  69.117 +
  69.118 +datatype 'a mixfix =
  69.119 +    Arg
  69.120 +  | Ignore
  69.121 +  | Module
  69.122 +  | Pretty of Pretty.T
  69.123 +  | Quote of 'a;
  69.124 +
  69.125 +fun is_arg Arg = true
  69.126 +  | is_arg Ignore = true
  69.127 +  | is_arg _ = false;
  69.128 +
  69.129 +fun quotes_of [] = []
  69.130 +  | quotes_of (Quote q :: ms) = q :: quotes_of ms
  69.131 +  | quotes_of (_ :: ms) = quotes_of ms;
  69.132 +
  69.133 +fun args_of [] xs = ([], xs)
  69.134 +  | args_of (Arg :: ms) (x :: xs) = apfst (cons x) (args_of ms xs)
  69.135 +  | args_of (Ignore :: ms) (_ :: xs) = args_of ms xs
  69.136 +  | args_of (_ :: ms) xs = args_of ms xs;
  69.137 +
  69.138 +fun num_args_of x = length (filter is_arg x);
  69.139 +
  69.140 +
  69.141 +(**** theory data ****)
  69.142 +
  69.143 +(* preprocessed definition table *)
  69.144 +
  69.145 +type deftab =
  69.146 +  (typ *              (* type of constant *)
  69.147 +    (string *         (* name of theory containing definition of constant *)
  69.148 +      thm))           (* definition theorem *)
  69.149 +  list Symtab.table;
  69.150 +
  69.151 +(* code dependency graph *)
  69.152 +
  69.153 +type nametab = (string * string) Symtab.table * unit Symtab.table;
  69.154 +
  69.155 +fun merge_nametabs ((tab, used) : nametab, (tab', used')) =
  69.156 +  (Symtab.merge op = (tab, tab'), Symtab.merge op = (used, used'));
  69.157 +
  69.158 +type node =
  69.159 +  (exn option *    (* slot for arbitrary data *)
  69.160 +   string *        (* name of structure containing piece of code *)
  69.161 +   string);        (* piece of code *)
  69.162 +
  69.163 +type codegr =
  69.164 +  node Graph.T *
  69.165 +  (nametab *       (* table for assigned constant names *)
  69.166 +   nametab);       (* table for assigned type names *)
  69.167 +
  69.168 +val emptygr : codegr = (Graph.empty,
  69.169 +  ((Symtab.empty, Symtab.empty), (Symtab.empty, Symtab.empty)));
  69.170 +
  69.171 +(* type of code generators *)
  69.172 +
  69.173 +type 'a codegen =
  69.174 +  theory ->      (* theory in which generate_code was called *)
  69.175 +  string list -> (* mode *)
  69.176 +  deftab ->      (* definition table (for efficiency) *)
  69.177 +  string ->      (* node name of caller (for recording dependencies) *)
  69.178 +  string ->      (* module name of caller (for modular code generation) *)
  69.179 +  bool ->        (* whether to parenthesize generated expression *)
  69.180 +  'a ->          (* item to generate code from *)
  69.181 +  codegr ->      (* code dependency graph *)
  69.182 +  (Pretty.T * codegr) option;
  69.183 +
  69.184 +
  69.185 +(* theory data *)
  69.186 +
  69.187 +structure CodegenData = Theory_Data
  69.188 +(
  69.189 +  type T =
  69.190 +    {codegens : (string * term codegen) list,
  69.191 +     tycodegens : (string * typ codegen) list,
  69.192 +     consts : ((string * typ) * (term mixfix list * (string * string) list)) list,
  69.193 +     types : (string * (typ mixfix list * (string * string) list)) list,
  69.194 +     preprocs: (stamp * (theory -> thm list -> thm list)) list,
  69.195 +     modules: codegr Symtab.table};
  69.196 +
  69.197 +  val empty =
  69.198 +    {codegens = [], tycodegens = [], consts = [], types = [],
  69.199 +     preprocs = [], modules = Symtab.empty};
  69.200 +  val extend = I;
  69.201 +
  69.202 +  fun merge
  69.203 +    ({codegens = codegens1, tycodegens = tycodegens1,
  69.204 +      consts = consts1, types = types1,
  69.205 +      preprocs = preprocs1, modules = modules1} : T,
  69.206 +     {codegens = codegens2, tycodegens = tycodegens2,
  69.207 +      consts = consts2, types = types2,
  69.208 +      preprocs = preprocs2, modules = modules2}) : T =
  69.209 +    {codegens = AList.merge (op =) (K true) (codegens1, codegens2),
  69.210 +     tycodegens = AList.merge (op =) (K true) (tycodegens1, tycodegens2),
  69.211 +     consts = AList.merge (op =) (K true) (consts1, consts2),
  69.212 +     types = AList.merge (op =) (K true) (types1, types2),
  69.213 +     preprocs = AList.merge (op =) (K true) (preprocs1, preprocs2),
  69.214 +     modules = Symtab.merge (K true) (modules1, modules2)};
  69.215 +);
  69.216 +
  69.217 +fun print_codegens thy =
  69.218 +  let val {codegens, tycodegens, ...} = CodegenData.get thy in
  69.219 +    Pretty.writeln (Pretty.chunks
  69.220 +      [Pretty.strs ("term code generators:" :: map fst codegens),
  69.221 +       Pretty.strs ("type code generators:" :: map fst tycodegens)])
  69.222 +  end;
  69.223 +
  69.224 +
  69.225 +
  69.226 +(**** access modules ****)
  69.227 +
  69.228 +fun get_modules thy = #modules (CodegenData.get thy);
  69.229 +
  69.230 +fun map_modules f thy =
  69.231 +  let val {codegens, tycodegens, consts, types, preprocs, modules} =
  69.232 +    CodegenData.get thy;
  69.233 +  in CodegenData.put {codegens = codegens, tycodegens = tycodegens,
  69.234 +    consts = consts, types = types, preprocs = preprocs,
  69.235 +    modules = f modules} thy
  69.236 +  end;
  69.237 +
  69.238 +
  69.239 +(**** add new code generators to theory ****)
  69.240 +
  69.241 +fun add_codegen name f thy =
  69.242 +  let val {codegens, tycodegens, consts, types, preprocs, modules} =
  69.243 +    CodegenData.get thy
  69.244 +  in (case AList.lookup (op =) codegens name of
  69.245 +      NONE => CodegenData.put {codegens = (name, f) :: codegens,
  69.246 +        tycodegens = tycodegens, consts = consts, types = types,
  69.247 +        preprocs = preprocs, modules = modules} thy
  69.248 +    | SOME _ => error ("Code generator " ^ name ^ " already declared"))
  69.249 +  end;
  69.250 +
  69.251 +fun add_tycodegen name f thy =
  69.252 +  let val {codegens, tycodegens, consts, types, preprocs, modules} =
  69.253 +    CodegenData.get thy
  69.254 +  in (case AList.lookup (op =) tycodegens name of
  69.255 +      NONE => CodegenData.put {tycodegens = (name, f) :: tycodegens,
  69.256 +        codegens = codegens, consts = consts, types = types,
  69.257 +        preprocs = preprocs, modules = modules} thy
  69.258 +    | SOME _ => error ("Code generator " ^ name ^ " already declared"))
  69.259 +  end;
  69.260 +
  69.261 +
  69.262 +(**** preprocessors ****)
  69.263 +
  69.264 +fun add_preprocessor p thy =
  69.265 +  let val {codegens, tycodegens, consts, types, preprocs, modules} =
  69.266 +    CodegenData.get thy
  69.267 +  in CodegenData.put {tycodegens = tycodegens,
  69.268 +    codegens = codegens, consts = consts, types = types,
  69.269 +    preprocs = (stamp (), p) :: preprocs,
  69.270 +    modules = modules} thy
  69.271 +  end;
  69.272 +
  69.273 +fun preprocess thy =
  69.274 +  let val {preprocs, ...} = CodegenData.get thy
  69.275 +  in fold (fn (_, f) => f thy) preprocs end;
  69.276 +
  69.277 +fun preprocess_term thy t =
  69.278 +  let
  69.279 +    val x = Free (singleton (Name.variant_list (Misc_Legacy.add_term_names (t, []))) "x", fastype_of t);
  69.280 +    (* fake definition *)
  69.281 +    val eq = Skip_Proof.make_thm thy (Logic.mk_equals (x, t));
  69.282 +    fun err () = error "preprocess_term: bad preprocessor"
  69.283 +  in case map prop_of (preprocess thy [eq]) of
  69.284 +      [Const ("==", _) $ x' $ t'] => if x = x' then t' else err ()
  69.285 +    | _ => err ()
  69.286 +  end;
  69.287 +
  69.288 +structure UnfoldData = Theory_Data
  69.289 +(
  69.290 +  type T = simpset;
  69.291 +  val empty = empty_ss;
  69.292 +  val extend = I;
  69.293 +  val merge = merge_ss;
  69.294 +);
  69.295 +
  69.296 +val map_unfold = UnfoldData.map;
  69.297 +val add_unfold = map_unfold o Simplifier.add_simp;
  69.298 +val del_unfold = map_unfold o Simplifier.del_simp;
  69.299 +
  69.300 +fun unfold_preprocessor thy =
  69.301 +  let val ss = Simplifier.global_context thy (UnfoldData.get thy)
  69.302 +  in map (Thm.transfer thy #> Simplifier.full_simplify ss) end;
  69.303 +
  69.304 +
  69.305 +(**** associate constants with target language code ****)
  69.306 +
  69.307 +fun gen_assoc_const prep_const (raw_const, syn) thy =
  69.308 +  let
  69.309 +    val {codegens, tycodegens, consts, types, preprocs, modules} =
  69.310 +      CodegenData.get thy;
  69.311 +    val (cname, T) = prep_const thy raw_const;
  69.312 +  in
  69.313 +    if num_args_of (fst syn) > length (binder_types T) then
  69.314 +      error ("More arguments than in corresponding type of " ^ cname)
  69.315 +    else case AList.lookup (op =) consts (cname, T) of
  69.316 +      NONE => CodegenData.put {codegens = codegens,
  69.317 +        tycodegens = tycodegens,
  69.318 +        consts = ((cname, T), syn) :: consts,
  69.319 +        types = types, preprocs = preprocs,
  69.320 +        modules = modules} thy
  69.321 +    | SOME _ => error ("Constant " ^ cname ^ " already associated with code")
  69.322 +  end;
  69.323 +
  69.324 +val assoc_const_i = gen_assoc_const (K I);
  69.325 +val assoc_const = gen_assoc_const Code.read_bare_const;
  69.326 +
  69.327 +
  69.328 +(**** associate types with target language types ****)
  69.329 +
  69.330 +fun assoc_type (s, syn) thy =
  69.331 +  let
  69.332 +    val {codegens, tycodegens, consts, types, preprocs, modules} =
  69.333 +      CodegenData.get thy;
  69.334 +    val tc = Sign.intern_type thy s;
  69.335 +  in
  69.336 +    case Symtab.lookup (snd (#types (Type.rep_tsig (Sign.tsig_of thy)))) tc of
  69.337 +      SOME (Type.LogicalType i) =>
  69.338 +        if num_args_of (fst syn) > i then
  69.339 +          error ("More arguments than corresponding type constructor " ^ s)
  69.340 +        else
  69.341 +          (case AList.lookup (op =) types tc of
  69.342 +            NONE => CodegenData.put {codegens = codegens,
  69.343 +              tycodegens = tycodegens, consts = consts,
  69.344 +              types = (tc, syn) :: types,
  69.345 +              preprocs = preprocs, modules = modules} thy
  69.346 +          | SOME _ => error ("Type " ^ tc ^ " already associated with code"))
  69.347 +    | _ => error ("Not a type constructor: " ^ s)
  69.348 +  end;
  69.349 +
  69.350 +fun get_assoc_type thy = AList.lookup (op =) ((#types o CodegenData.get) thy);
  69.351 +
  69.352 +
  69.353 +(**** make valid ML identifiers ****)
  69.354 +
  69.355 +fun is_ascii_letdig x = Symbol.is_ascii_letter x orelse
  69.356 +  Symbol.is_ascii_digit x orelse Symbol.is_ascii_quasi x;
  69.357 +
  69.358 +fun dest_sym s =
  69.359 +  (case split_last (snd (take_prefix (fn c => c = "\\") (raw_explode s))) of
  69.360 +    ("<" :: "^" :: xs, ">") => (true, implode xs)
  69.361 +  | ("<" :: xs, ">") => (false, implode xs)
  69.362 +  | _ => raise Fail "dest_sym");
  69.363 +
  69.364 +fun mk_id s = if s = "" then "" else
  69.365 +  let
  69.366 +    fun check_str [] = []
  69.367 +      | check_str xs = (case take_prefix is_ascii_letdig xs of
  69.368 +          ([], " " :: zs) => check_str zs
  69.369 +        | ([], z :: zs) =>
  69.370 +          if size z = 1 then string_of_int (ord z) :: check_str zs
  69.371 +          else (case dest_sym z of
  69.372 +              (true, "isub") => check_str zs
  69.373 +            | (true, "isup") => "" :: check_str zs
  69.374 +            | (ctrl, s') => (if ctrl then "ctrl_" ^ s' else s') :: check_str zs)
  69.375 +        | (ys, zs) => implode ys :: check_str zs);
  69.376 +    val s' = space_implode "_" (maps (check_str o Symbol.explode) (Long_Name.explode s))
  69.377 +  in
  69.378 +    if Symbol.is_ascii_letter (hd (raw_explode s')) then s' else "id_" ^ s'
  69.379 +  end;
  69.380 +
  69.381 +fun mk_long_id (p as (tab, used)) module s =
  69.382 +  let
  69.383 +    fun find_name [] = raise Fail "mk_long_id"
  69.384 +      | find_name (ys :: yss) =
  69.385 +          let
  69.386 +            val s' = Long_Name.implode ys
  69.387 +            val s'' = Long_Name.append module s'
  69.388 +          in case Symtab.lookup used s'' of
  69.389 +              NONE => ((module, s'),
  69.390 +                (Symtab.update_new (s, (module, s')) tab,
  69.391 +                 Symtab.update_new (s'', ()) used))
  69.392 +            | SOME _ => find_name yss
  69.393 +          end
  69.394 +  in case Symtab.lookup tab s of
  69.395 +      NONE => find_name (Library.suffixes1 (Long_Name.explode s))
  69.396 +    | SOME name => (name, p)
  69.397 +  end;
  69.398 +
  69.399 +(* module:  module name for caller                                        *)
  69.400 +(* module': module name for callee                                        *)
  69.401 +(* if caller and callee reside in different modules, use qualified access *)
  69.402 +
  69.403 +fun mk_qual_id module (module', s) =
  69.404 +  if module = module' orelse module' = "" then s else module' ^ "." ^ s;
  69.405 +
  69.406 +fun mk_const_id module cname (gr, (tab1, tab2)) =
  69.407 +  let
  69.408 +    val ((module, s), tab1') = mk_long_id tab1 module cname
  69.409 +    val s' = mk_id s;
  69.410 +    val s'' = if ML_Syntax.is_reserved s' then s' ^ "_const" else s'
  69.411 +  in (((module, s'')), (gr, (tab1', tab2))) end;
  69.412 +
  69.413 +fun get_const_id (gr, (tab1, tab2)) cname =
  69.414 +  case Symtab.lookup (fst tab1) cname of
  69.415 +    NONE => error ("get_const_id: no such constant: " ^ quote cname)
  69.416 +  | SOME (module, s) =>
  69.417 +      let
  69.418 +        val s' = mk_id s;
  69.419 +        val s'' = if ML_Syntax.is_reserved s' then s' ^ "_const" else s'
  69.420 +      in (module, s'') end;
  69.421 +
  69.422 +fun mk_type_id module tyname (gr, (tab1, tab2)) =
  69.423 +  let
  69.424 +    val ((module, s), tab2') = mk_long_id tab2 module tyname
  69.425 +    val s' = mk_id s;
  69.426 +    val s'' = if ML_Syntax.is_reserved s' then s' ^ "_type" else s'
  69.427 +  in ((module, s''), (gr, (tab1, tab2'))) end;
  69.428 +
  69.429 +fun get_type_id (gr, (tab1, tab2)) tyname =
  69.430 +  case Symtab.lookup (fst tab2) tyname of
  69.431 +    NONE => error ("get_type_id: no such type: " ^ quote tyname)
  69.432 +  | SOME (module, s) =>
  69.433 +      let
  69.434 +        val s' = mk_id s;
  69.435 +        val s'' = if ML_Syntax.is_reserved s' then s' ^ "_type" else s'
  69.436 +      in (module, s'') end;
  69.437 +
  69.438 +fun get_type_id' f tab tyname = apsnd f (get_type_id tab tyname);
  69.439 +
  69.440 +fun get_node (gr, x) k = Graph.get_node gr k;
  69.441 +fun add_edge e (gr, x) = (Graph.add_edge e gr, x);
  69.442 +fun add_edge_acyclic e (gr, x) = (Graph.add_edge_acyclic e gr, x);
  69.443 +fun del_nodes ks (gr, x) = (Graph.del_nodes ks gr, x);
  69.444 +fun map_node k f (gr, x) = (Graph.map_node k f gr, x);
  69.445 +fun new_node p (gr, x) = (Graph.new_node p gr, x);
  69.446 +
  69.447 +fun thyname_of_type thy = #theory_name o Name_Space.the_entry (Sign.type_space thy);
  69.448 +fun thyname_of_const thy = #theory_name o Name_Space.the_entry (Sign.const_space thy);
  69.449 +
  69.450 +fun rename_terms ts =
  69.451 +  let
  69.452 +    val names = List.foldr Misc_Legacy.add_term_names
  69.453 +      (map (fst o fst) (rev (fold Term.add_vars ts []))) ts;
  69.454 +    val reserved = filter ML_Syntax.is_reserved names;
  69.455 +    val (illegal, alt_names) = split_list (map_filter (fn s =>
  69.456 +      let val s' = mk_id s in if s = s' then NONE else SOME (s, s') end) names)
  69.457 +    val ps = (reserved @ illegal) ~~
  69.458 +      Name.variant_list names (map (suffix "'") reserved @ alt_names);
  69.459 +
  69.460 +    fun rename_id s = AList.lookup (op =) ps s |> the_default s;
  69.461 +
  69.462 +    fun rename (Var ((a, i), T)) = Var ((rename_id a, i), T)
  69.463 +      | rename (Free (a, T)) = Free (rename_id a, T)
  69.464 +      | rename (Abs (s, T, t)) = Abs (s, T, rename t)
  69.465 +      | rename (t $ u) = rename t $ rename u
  69.466 +      | rename t = t;
  69.467 +  in
  69.468 +    map rename ts
  69.469 +  end;
  69.470 +
  69.471 +val rename_term = hd o rename_terms o single;
  69.472 +
  69.473 +
  69.474 +(**** retrieve definition of constant ****)
  69.475 +
  69.476 +fun is_instance T1 T2 =
  69.477 +  Type.raw_instance (T1, if null (Misc_Legacy.typ_tfrees T2) then T2 else Logic.varifyT_global T2);
  69.478 +
  69.479 +fun get_assoc_code thy (s, T) = Option.map snd (find_first (fn ((s', T'), _) =>
  69.480 +  s = s' andalso is_instance T T') (#consts (CodegenData.get thy)));
  69.481 +
  69.482 +fun get_aux_code mode xs = map_filter (fn (m, code) =>
  69.483 +  if m = "" orelse member (op =) mode m then SOME code else NONE) xs;
  69.484 +
  69.485 +fun dest_prim_def t =
  69.486 +  let
  69.487 +    val (lhs, rhs) = Logic.dest_equals t;
  69.488 +    val (c, args) = strip_comb lhs;
  69.489 +    val (s, T) = dest_Const c
  69.490 +  in if forall is_Var args then SOME (s, (T, (args, rhs))) else NONE
  69.491 +  end handle TERM _ => NONE;
  69.492 +
  69.493 +fun mk_deftab thy =
  69.494 +  let
  69.495 +    val axmss =
  69.496 +      map (fn thy' => (Context.theory_name thy', Theory.axiom_table thy'))
  69.497 +        (Theory.nodes_of thy);
  69.498 +    fun add_def thyname (name, t) =
  69.499 +      (case dest_prim_def t of
  69.500 +        NONE => I
  69.501 +      | SOME (s, (T, _)) => Symtab.map_default (s, [])
  69.502 +          (cons (T, (thyname, Thm.axiom thy name))));
  69.503 +  in
  69.504 +    fold (fn (thyname, axms) => Symtab.fold (add_def thyname) axms) axmss Symtab.empty
  69.505 +  end;
  69.506 +
  69.507 +fun prep_prim_def thy thm =
  69.508 +  let
  69.509 +    val prop = case preprocess thy [thm]
  69.510 +     of [thm'] => Thm.prop_of thm'
  69.511 +      | _ => error "mk_deftab: bad preprocessor"
  69.512 +  in ((Option.map o apsnd o apsnd)
  69.513 +    (fn (args, rhs) => split_last (rename_terms (args @ [rhs]))) o dest_prim_def) prop
  69.514 +  end;
  69.515 +
  69.516 +fun get_defn thy defs s T = (case Symtab.lookup defs s of
  69.517 +    NONE => NONE
  69.518 +  | SOME ds =>
  69.519 +      let val i = find_index (is_instance T o fst) ds
  69.520 +      in if i >= 0 then
  69.521 +          SOME (nth ds i, if length ds = 1 then NONE else SOME i)
  69.522 +        else NONE
  69.523 +      end);
  69.524 +
  69.525 +
  69.526 +(**** invoke suitable code generator for term / type ****)
  69.527 +
  69.528 +fun codegen_error (gr, _) dep s =
  69.529 +  error (s ^ "\nrequired by:\n" ^ commas (Graph.all_succs gr [dep]));
  69.530 +
  69.531 +fun invoke_codegen thy mode defs dep module brack t gr = (case get_first
  69.532 +   (fn (_, f) => f thy mode defs dep module brack t gr) (#codegens (CodegenData.get thy)) of
  69.533 +      NONE => codegen_error gr dep ("Unable to generate code for term:\n" ^
  69.534 +        Syntax.string_of_term_global thy t)
  69.535 +    | SOME x => x);
  69.536 +
  69.537 +fun invoke_tycodegen thy mode defs dep module brack T gr = (case get_first
  69.538 +   (fn (_, f) => f thy mode defs dep module brack T gr ) (#tycodegens (CodegenData.get thy)) of
  69.539 +      NONE => codegen_error gr dep ("Unable to generate code for type:\n" ^
  69.540 +        Syntax.string_of_typ_global thy T)
  69.541 +    | SOME x => x);
  69.542 +
  69.543 +
  69.544 +(**** code generator for mixfix expressions ****)
  69.545 +
  69.546 +fun parens p = Pretty.block [str "(", p, str ")"];
  69.547 +
  69.548 +fun pretty_fn [] p = [p]
  69.549 +  | pretty_fn (x::xs) p = str ("fn " ^ x ^ " =>") ::
  69.550 +      Pretty.brk 1 :: pretty_fn xs p;
  69.551 +
  69.552 +fun pretty_mixfix _ _ [] [] _ = []
  69.553 +  | pretty_mixfix module module' (Arg :: ms) (p :: ps) qs =
  69.554 +      p :: pretty_mixfix module module' ms ps qs
  69.555 +  | pretty_mixfix module module' (Ignore :: ms) ps qs =
  69.556 +      pretty_mixfix module module' ms ps qs
  69.557 +  | pretty_mixfix module module' (Module :: ms) ps qs =
  69.558 +      (if module <> module'
  69.559 +       then cons (str (module' ^ ".")) else I)
  69.560 +      (pretty_mixfix module module' ms ps qs)
  69.561 +  | pretty_mixfix module module' (Pretty p :: ms) ps qs =
  69.562 +      p :: pretty_mixfix module module' ms ps qs
  69.563 +  | pretty_mixfix module module' (Quote _ :: ms) ps (q :: qs) =
  69.564 +      q :: pretty_mixfix module module' ms ps qs;
  69.565 +
  69.566 +fun replace_quotes [] [] = []
  69.567 +  | replace_quotes xs (Arg :: ms) =
  69.568 +      Arg :: replace_quotes xs ms
  69.569 +  | replace_quotes xs (Ignore :: ms) =
  69.570 +      Ignore :: replace_quotes xs ms
  69.571 +  | replace_quotes xs (Module :: ms) =
  69.572 +      Module :: replace_quotes xs ms
  69.573 +  | replace_quotes xs (Pretty p :: ms) =
  69.574 +      Pretty p :: replace_quotes xs ms
  69.575 +  | replace_quotes (x::xs) (Quote _ :: ms) =
  69.576 +      Quote x :: replace_quotes xs ms;
  69.577 +
  69.578 +
  69.579 +(**** default code generators ****)
  69.580 +
  69.581 +fun eta_expand t ts i =
  69.582 +  let
  69.583 +    val k = length ts;
  69.584 +    val Ts = drop k (binder_types (fastype_of t));
  69.585 +    val j = i - k
  69.586 +  in
  69.587 +    List.foldr (fn (T, t) => Abs ("x", T, t))
  69.588 +      (list_comb (t, ts @ map Bound (j-1 downto 0))) (take j Ts)
  69.589 +  end;
  69.590 +
  69.591 +fun mk_app _ p [] = p
  69.592 +  | mk_app brack p ps = if brack then
  69.593 +       Pretty.block (str "(" ::
  69.594 +         separate (Pretty.brk 1) (p :: ps) @ [str ")"])
  69.595 +     else Pretty.block (separate (Pretty.brk 1) (p :: ps));
  69.596 +
  69.597 +fun new_names t xs = Name.variant_list
  69.598 +  (union (op =) (map (fst o fst o dest_Var) (Misc_Legacy.term_vars t))
  69.599 +    (Misc_Legacy.add_term_names (t, ML_Syntax.reserved_names))) (map mk_id xs);
  69.600 +
  69.601 +fun new_name t x = hd (new_names t [x]);
  69.602 +
  69.603 +fun if_library mode x y = if member (op =) mode "library" then x else y;
  69.604 +
  69.605 +fun default_codegen thy mode defs dep module brack t gr =
  69.606 +  let
  69.607 +    val (u, ts) = strip_comb t;
  69.608 +    fun codegens brack = fold_map (invoke_codegen thy mode defs dep module brack)
  69.609 +  in (case u of
  69.610 +      Var ((s, i), T) =>
  69.611 +        let
  69.612 +          val (ps, gr') = codegens true ts gr;
  69.613 +          val (_, gr'') = invoke_tycodegen thy mode defs dep module false T gr'
  69.614 +        in SOME (mk_app brack (str (s ^
  69.615 +           (if i=0 then "" else string_of_int i))) ps, gr'')
  69.616 +        end
  69.617 +
  69.618 +    | Free (s, T) =>
  69.619 +        let
  69.620 +          val (ps, gr') = codegens true ts gr;
  69.621 +          val (_, gr'') = invoke_tycodegen thy mode defs dep module false T gr'
  69.622 +        in SOME (mk_app brack (str s) ps, gr'') end
  69.623 +
  69.624 +    | Const (s, T) =>
  69.625 +      (case get_assoc_code thy (s, T) of
  69.626 +         SOME (ms, aux) =>
  69.627 +           let val i = num_args_of ms
  69.628 +           in if length ts < i then
  69.629 +               default_codegen thy mode defs dep module brack (eta_expand u ts i) gr 
  69.630 +             else
  69.631 +               let
  69.632 +                 val (ts1, ts2) = args_of ms ts;
  69.633 +                 val (ps1, gr1) = codegens false ts1 gr;
  69.634 +                 val (ps2, gr2) = codegens true ts2 gr1;
  69.635 +                 val (ps3, gr3) = codegens false (quotes_of ms) gr2;
  69.636 +                 val (_, gr4) = invoke_tycodegen thy mode defs dep module false
  69.637 +                   (funpow (length ts) (hd o tl o snd o dest_Type) T) gr3;
  69.638 +                 val (module', suffix) = (case get_defn thy defs s T of
  69.639 +                     NONE => (if_library mode (thyname_of_const thy s) module, "")
  69.640 +                   | SOME ((U, (module', _)), NONE) =>
  69.641 +                       (if_library mode module' module, "")
  69.642 +                   | SOME ((U, (module', _)), SOME i) =>
  69.643 +                       (if_library mode module' module, " def" ^ string_of_int i));
  69.644 +                 val node_id = s ^ suffix;
  69.645 +                 fun p module' = mk_app brack (Pretty.block
  69.646 +                   (pretty_mixfix module module' ms ps1 ps3)) ps2
  69.647 +               in SOME (case try (get_node gr4) node_id of
  69.648 +                   NONE => (case get_aux_code mode aux of
  69.649 +                       [] => (p module, gr4)
  69.650 +                     | xs => (p module', add_edge (node_id, dep) (new_node
  69.651 +                         (node_id, (NONE, module', cat_lines xs ^ "\n")) gr4)))
  69.652 +                 | SOME (_, module'', _) =>
  69.653 +                     (p module'', add_edge (node_id, dep) gr4))
  69.654 +               end
  69.655 +           end
  69.656 +       | NONE => (case get_defn thy defs s T of
  69.657 +           NONE => NONE
  69.658 +         | SOME ((U, (thyname, thm)), k) => (case prep_prim_def thy thm
  69.659 +            of SOME (_, (_, (args, rhs))) => let
  69.660 +               val module' = if_library mode thyname module;
  69.661 +               val suffix = (case k of NONE => "" | SOME i => " def" ^ string_of_int i);
  69.662 +               val node_id = s ^ suffix;
  69.663 +               val ((ps, def_id), gr') = gr |> codegens true ts
  69.664 +                 ||>> mk_const_id module' (s ^ suffix);
  69.665 +               val p = mk_app brack (str (mk_qual_id module def_id)) ps
  69.666 +             in SOME (case try (get_node gr') node_id of
  69.667 +                 NONE =>
  69.668 +                   let
  69.669 +                     val _ = message ("expanding definition of " ^ s);
  69.670 +                     val Ts = binder_types U;
  69.671 +                     val (args', rhs') =
  69.672 +                       if not (null args) orelse null Ts then (args, rhs) else
  69.673 +                         let val v = Free (new_name rhs "x", hd Ts)
  69.674 +                         in ([v], betapply (rhs, v)) end;
  69.675 +                     val (p', gr1) = invoke_codegen thy mode defs node_id module' false
  69.676 +                       rhs' (add_edge (node_id, dep)
  69.677 +                          (new_node (node_id, (NONE, "", "")) gr'));
  69.678 +                     val (xs, gr2) = codegens false args' gr1;
  69.679 +                     val (_, gr3) = invoke_tycodegen thy mode defs dep module false T gr2;
  69.680 +                     val (ty, gr4) = invoke_tycodegen thy mode defs node_id module' false U gr3;
  69.681 +                   in (p, map_node node_id (K (NONE, module', string_of
  69.682 +                       (Pretty.block (separate (Pretty.brk 1)
  69.683 +                         (if null args' then
  69.684 +                            [str ("val " ^ snd def_id ^ " :"), ty]
  69.685 +                          else str ("fun " ^ snd def_id) :: xs) @
  69.686 +                        [str " =", Pretty.brk 1, p', str ";"])) ^ "\n\n")) gr4)
  69.687 +                   end
  69.688 +               | SOME _ => (p, add_edge (node_id, dep) gr'))
  69.689 +             end
  69.690 +             | NONE => NONE)))
  69.691 +
  69.692 +    | Abs _ =>
  69.693 +      let
  69.694 +        val (bs, Ts) = ListPair.unzip (strip_abs_vars u);
  69.695 +        val t = strip_abs_body u
  69.696 +        val bs' = new_names t bs;
  69.697 +        val (ps, gr1) = codegens true ts gr;
  69.698 +        val (p, gr2) = invoke_codegen thy mode defs dep module false
  69.699 +          (subst_bounds (map Free (rev (bs' ~~ Ts)), t)) gr1;
  69.700 +      in
  69.701 +        SOME (mk_app brack (Pretty.block (str "(" :: pretty_fn bs' p @
  69.702 +          [str ")"])) ps, gr2)
  69.703 +      end
  69.704 +
  69.705 +    | _ => NONE)
  69.706 +  end;
  69.707 +
  69.708 +fun default_tycodegen thy mode defs dep module brack (TVar ((s, i), _)) gr =
  69.709 +      SOME (str (s ^ (if i = 0 then "" else string_of_int i)), gr)
  69.710 +  | default_tycodegen thy mode defs dep module brack (TFree (s, _)) gr =
  69.711 +      SOME (str s, gr)
  69.712 +  | default_tycodegen thy mode defs dep module brack (Type (s, Ts)) gr =
  69.713 +      (case AList.lookup (op =) ((#types o CodegenData.get) thy) s of
  69.714 +         NONE => NONE
  69.715 +       | SOME (ms, aux) =>
  69.716 +           let
  69.717 +             val (ps, gr') = fold_map
  69.718 +               (invoke_tycodegen thy mode defs dep module false)
  69.719 +               (fst (args_of ms Ts)) gr;
  69.720 +             val (qs, gr'') = fold_map
  69.721 +               (invoke_tycodegen thy mode defs dep module false)
  69.722 +               (quotes_of ms) gr';
  69.723 +             val module' = if_library mode (thyname_of_type thy s) module;
  69.724 +             val node_id = s ^ " (type)";
  69.725 +             fun p module' = Pretty.block (pretty_mixfix module module' ms ps qs)
  69.726 +           in SOME (case try (get_node gr'') node_id of
  69.727 +               NONE => (case get_aux_code mode aux of
  69.728 +                   [] => (p module', gr'')
  69.729 +                 | xs => (p module', snd (mk_type_id module' s
  69.730 +                       (add_edge (node_id, dep) (new_node (node_id,
  69.731 +                         (NONE, module', cat_lines xs ^ "\n")) gr'')))))
  69.732 +             | SOME (_, module'', _) =>
  69.733 +                 (p module'', add_edge (node_id, dep) gr''))
  69.734 +           end);
  69.735 +
  69.736 +fun mk_tuple [p] = p
  69.737 +  | mk_tuple ps = Pretty.block (str "(" ::
  69.738 +      flat (separate [str ",", Pretty.brk 1] (map single ps)) @ [str ")"]);
  69.739 +
  69.740 +fun mk_let bindings body =
  69.741 +  Pretty.blk (0, [str "let", Pretty.brk 1,
  69.742 +    Pretty.blk (0, separate Pretty.fbrk (map (fn (pat, rhs) =>
  69.743 +      Pretty.block [str "val ", pat, str " =", Pretty.brk 1,
  69.744 +      rhs, str ";"]) bindings)),
  69.745 +    Pretty.brk 1, str "in", Pretty.brk 1, body,
  69.746 +    Pretty.brk 1, str "end"]);
  69.747 +
  69.748 +fun mk_struct name s = "structure " ^ name ^ " =\nstruct\n\n" ^ s ^ "end;\n";
  69.749 +
  69.750 +fun add_to_module name s = AList.map_entry (op =) (name : string) (suffix s);
  69.751 +
  69.752 +fun output_code gr module xs =
  69.753 +  let
  69.754 +    val code = map_filter (fn s =>
  69.755 +      let val c as (_, module', _) = Graph.get_node gr s
  69.756 +      in if module = "" orelse module = module' then SOME (s, c) else NONE end)
  69.757 +        (rev (Graph.all_preds gr xs));
  69.758 +    fun string_of_cycle (a :: b :: cs) =
  69.759 +          let val SOME (x, y) = get_first (fn (x, (_, a', _)) =>
  69.760 +            if a = a' then Option.map (pair x)
  69.761 +              (find_first ((fn (_, b', _) => b' = b) o Graph.get_node gr)
  69.762 +                (Graph.imm_succs gr x))
  69.763 +            else NONE) code
  69.764 +          in x ^ " called by " ^ y ^ "\n" ^ string_of_cycle (b :: cs) end
  69.765 +      | string_of_cycle _ = ""
  69.766 +  in
  69.767 +    if module = "" then
  69.768 +      let
  69.769 +        val modules = distinct (op =) (map (#2 o snd) code);
  69.770 +        val mod_gr = fold_rev Graph.add_edge_acyclic
  69.771 +          (maps (fn (s, (_, module, _)) => map (pair module)
  69.772 +            (filter_out (fn s => s = module) (map (#2 o Graph.get_node gr)
  69.773 +              (Graph.imm_succs gr s)))) code)
  69.774 +          (fold_rev (Graph.new_node o rpair ()) modules Graph.empty);
  69.775 +        val modules' =
  69.776 +          rev (Graph.all_preds mod_gr (map (#2 o Graph.get_node gr) xs))
  69.777 +      in
  69.778 +        List.foldl (fn ((_, (_, module, s)), ms) => add_to_module module s ms)
  69.779 +          (map (rpair "") modules') code
  69.780 +      end handle Graph.CYCLES (cs :: _) =>
  69.781 +        error ("Cyclic dependency of modules:\n" ^ commas cs ^
  69.782 +          "\n" ^ string_of_cycle cs)
  69.783 +    else [(module, implode (map (#3 o snd) code))]
  69.784 +  end;
  69.785 +
  69.786 +fun gen_generate_code prep_term thy mode modules module xs =
  69.787 +  let
  69.788 +    val _ = (module <> "" orelse
  69.789 +        member (op =) mode "library" andalso forall (fn (s, _) => s = "") xs)
  69.790 +      orelse error "missing module name";
  69.791 +    val graphs = get_modules thy;
  69.792 +    val defs = mk_deftab thy;
  69.793 +    val gr = new_node ("<Top>", (NONE, module, ""))
  69.794 +      (List.foldl (fn ((gr, (tab1, tab2)), (gr', (tab1', tab2'))) =>
  69.795 +        (Graph.merge (fn ((_, module, _), (_, module', _)) =>
  69.796 +           module = module') (gr, gr'),
  69.797 +         (merge_nametabs (tab1, tab1'), merge_nametabs (tab2, tab2')))) emptygr
  69.798 +           (map (fn s => case Symtab.lookup graphs s of
  69.799 +                NONE => error ("Undefined code module: " ^ s)
  69.800 +              | SOME gr => gr) modules))
  69.801 +      handle Graph.DUP k => error ("Duplicate code for " ^ k);
  69.802 +    fun expand (t as Abs _) = t
  69.803 +      | expand t = (case fastype_of t of
  69.804 +          Type ("fun", [T, U]) => Abs ("x", T, t $ Bound 0) | _ => t);
  69.805 +    val (ps, gr') = fold_map (fn (s, t) => fn gr => apfst (pair s)
  69.806 +      (invoke_codegen thy mode defs "<Top>" module false t gr))
  69.807 +        (map (apsnd (expand o preprocess_term thy o prep_term thy)) xs) gr;
  69.808 +    val code = map_filter
  69.809 +      (fn ("", _) => NONE
  69.810 +        | (s', p) => SOME (string_of (Pretty.block
  69.811 +          [str ("val " ^ s' ^ " ="), Pretty.brk 1, p, str ";"]))) ps;
  69.812 +    val code' = space_implode "\n\n" code ^ "\n\n";
  69.813 +    val code'' =
  69.814 +      map_filter (fn (name, s) =>
  69.815 +          if member (op =) mode "library" andalso name = module andalso null code
  69.816 +          then NONE
  69.817 +          else SOME (name, mk_struct name s))
  69.818 +        ((if null code then I
  69.819 +          else add_to_module module code')
  69.820 +           (output_code (fst gr') (if_library mode "" module) ["<Top>"]))
  69.821 +  in
  69.822 +    (code'', del_nodes ["<Top>"] gr')
  69.823 +  end;
  69.824 +
  69.825 +val generate_code_i = gen_generate_code Sign.cert_term;
  69.826 +val generate_code =
  69.827 +  gen_generate_code (Syntax.read_term o Proof_Context.allow_dummies o Proof_Context.init_global);
  69.828 +
  69.829 +
  69.830 +(**** Reflection ****)
  69.831 +
  69.832 +val strip_tname = implode o tl o raw_explode;
  69.833 +
  69.834 +fun pretty_list xs = Pretty.block (str "[" ::
  69.835 +  flat (separate [str ",", Pretty.brk 1] (map single xs)) @
  69.836 +  [str "]"]);
  69.837 +
  69.838 +fun mk_type p (TVar ((s, i), _)) = str
  69.839 +      (strip_tname s ^ (if i = 0 then "" else string_of_int i) ^ "T")
  69.840 +  | mk_type p (TFree (s, _)) = str (strip_tname s ^ "T")
  69.841 +  | mk_type p (Type (s, Ts)) = (if p then parens else I) (Pretty.block
  69.842 +      [str "Type", Pretty.brk 1, str ("(\"" ^ s ^ "\","),
  69.843 +       Pretty.brk 1, pretty_list (map (mk_type false) Ts), str ")"]);
  69.844 +
  69.845 +fun mk_term_of gr module p (TVar ((s, i), _)) = str
  69.846 +      (strip_tname s ^ (if i = 0 then "" else string_of_int i) ^ "F")
  69.847 +  | mk_term_of gr module p (TFree (s, _)) = str (strip_tname s ^ "F")
  69.848 +  | mk_term_of gr module p (Type (s, Ts)) = (if p then parens else I)
  69.849 +      (Pretty.block (separate (Pretty.brk 1)
  69.850 +        (str (mk_qual_id module
  69.851 +          (get_type_id' (fn s' => "term_of_" ^ s') gr s)) ::
  69.852 +        maps (fn T =>
  69.853 +          [mk_term_of gr module true T, mk_type true T]) Ts)));
  69.854 +
  69.855 +
  69.856 +(**** Implicit results ****)
  69.857 +
  69.858 +structure Result = Proof_Data
  69.859 +(
  69.860 +  type T = (int -> term list option) * (unit -> term);
  69.861 +  fun init _ = (fn _ => NONE, fn () => Bound 0);
  69.862 +);
  69.863 +
  69.864 +val get_test_fn = #1 o Result.get;
  69.865 +val get_eval_fn = #2 o Result.get;
  69.866 +
  69.867 +fun poke_test_fn f = Context.>> (Context.map_proof (Result.map (fn (_, g) => (f, g))));
  69.868 +fun poke_eval_fn g = Context.>> (Context.map_proof (Result.map (fn (f, _) => (f, g))));
  69.869 +
  69.870 +
  69.871 +(**** Test data generators ****)
  69.872 +
  69.873 +fun mk_gen gr module p xs a (TVar ((s, i), _)) = str
  69.874 +      (strip_tname s ^ (if i = 0 then "" else string_of_int i) ^ "G")
  69.875 +  | mk_gen gr module p xs a (TFree (s, _)) = str (strip_tname s ^ "G")
  69.876 +  | mk_gen gr module p xs a (Type (tyc as (s, Ts))) = (if p then parens else I)
  69.877 +      (Pretty.block (separate (Pretty.brk 1)
  69.878 +        (str (mk_qual_id module (get_type_id' (fn s' => "gen_" ^ s') gr s) ^
  69.879 +          (if member (op =) xs s then "'" else "")) ::
  69.880 +         (case tyc of
  69.881 +            ("fun", [T, U]) =>
  69.882 +              [mk_term_of gr module true T, mk_type true T,
  69.883 +               mk_gen gr module true xs a U, mk_type true U]
  69.884 +          | _ => maps (fn T =>
  69.885 +              [mk_gen gr module true xs a T, mk_type true T]) Ts) @
  69.886 +         (if member (op =) xs s then [str a] else []))));
  69.887 +
  69.888 +fun test_term ctxt t =
  69.889 +  let
  69.890 +    val thy = Proof_Context.theory_of ctxt;
  69.891 +    val (code, gr) = generate_code_i thy ["term_of", "test"] [] "Generated" [("testf", t)];
  69.892 +    val Ts = map snd (fst (strip_abs t));
  69.893 +    val args = map_index (fn (i, T) => ("arg" ^ string_of_int i, T)) Ts;
  69.894 +    val s = "structure Test_Term =\nstruct\n\n" ^
  69.895 +      cat_lines (map snd code) ^
  69.896 +      "\nopen Generated;\n\n" ^ string_of
  69.897 +        (Pretty.block [str "val () = Codegen.poke_test_fn",
  69.898 +          Pretty.brk 1, str ("(fn i =>"), Pretty.brk 1,
  69.899 +          mk_let (map (fn (s, T) =>
  69.900 +              (mk_tuple [str s, str (s ^ "_t")],
  69.901 +               Pretty.block [mk_gen gr "Generated" false [] "" T, Pretty.brk 1,
  69.902 +                 str "i"])) args)
  69.903 +            (Pretty.block [str "if ",
  69.904 +              mk_app false (str "testf") (map (str o fst) args),
  69.905 +              Pretty.brk 1, str "then NONE",
  69.906 +              Pretty.brk 1, str "else ",
  69.907 +              Pretty.block [str "SOME ",
  69.908 +                Pretty.enum "," "[" "]" (map (fn (s, _) => str (s ^ "_t ()")) args)]]),
  69.909 +          str ");"]) ^
  69.910 +      "\n\nend;\n";
  69.911 +  in
  69.912 +    ctxt
  69.913 +    |> Context.proof_map (ML_Context.exec (fn () => ML_Context.eval_text false Position.none s))
  69.914 +    |> get_test_fn
  69.915 +  end;
  69.916 +
  69.917 +
  69.918 +(**** Evaluator for terms ****)
  69.919 +
  69.920 +fun eval_term ctxt t =
  69.921 +  let
  69.922 +    val _ =
  69.923 +      legacy_feature
  69.924 +        "Old evaluation mechanism -- use evaluator \"code\" or method \"eval\" instead";
  69.925 +    val thy = Proof_Context.theory_of ctxt;
  69.926 +    val _ = (null (Term.add_tvars t []) andalso null (Term.add_tfrees t [])) orelse
  69.927 +      error "Term to be evaluated contains type variables";
  69.928 +    val _ = (null (Term.add_vars t []) andalso null (Term.add_frees t [])) orelse
  69.929 +      error "Term to be evaluated contains variables";
  69.930 +    val (code, gr) =
  69.931 +      generate_code_i thy ["term_of"] [] "Generated"
  69.932 +        [("result", Abs ("x", TFree ("'a", []), t))];
  69.933 +    val s = "structure Eval_Term =\nstruct\n\n" ^
  69.934 +      cat_lines (map snd code) ^
  69.935 +      "\nopen Generated;\n\n" ^ string_of
  69.936 +        (Pretty.block [str "val () = Codegen.poke_eval_fn (fn () =>",
  69.937 +          Pretty.brk 1,
  69.938 +          mk_app false (mk_term_of gr "Generated" false (fastype_of t))
  69.939 +            [str "(result ())"],
  69.940 +          str ");"]) ^
  69.941 +      "\n\nend;\n";
  69.942 +    val eval_fn =
  69.943 +      ctxt
  69.944 +      |> Context.proof_map (ML_Context.exec (fn () => ML_Context.eval_text false Position.none s))
  69.945 +      |> get_eval_fn;
  69.946 +  in eval_fn () end;
  69.947 +
  69.948 +val (_, evaluation_oracle) = Context.>>> (Context.map_theory_result
  69.949 +  (Thm.add_oracle (Binding.name "evaluation", fn (ctxt, ct) =>
  69.950 +    let
  69.951 +      val thy = Proof_Context.theory_of ctxt;
  69.952 +      val t = Thm.term_of ct;
  69.953 +    in
  69.954 +      if Theory.subthy (Thm.theory_of_cterm ct, thy) then
  69.955 +        Thm.cterm_of thy (Logic.mk_equals (t, eval_term ctxt t))
  69.956 +      else raise CTERM ("evaluation_oracle: bad theory", [ct])
  69.957 +    end)));
  69.958 +
  69.959 +fun evaluation_conv ctxt ct = evaluation_oracle (ctxt, ct);
  69.960 +
  69.961 +
  69.962 +(**** Interface ****)
  69.963 +
  69.964 +fun parse_mixfix rd s =
  69.965 +  (case Scan.finite Symbol.stopper (Scan.repeat
  69.966 +     (   $$ "_" >> K Arg
  69.967 +      || $$ "?" >> K Ignore
  69.968 +      || $$ "\<module>" >> K Module
  69.969 +      || $$ "/" |-- Scan.repeat ($$ " ") >> (Pretty o Pretty.brk o length)
  69.970 +      || $$ "{" |-- $$ "*" |-- Scan.repeat1
  69.971 +           (   $$ "'" |-- Scan.one Symbol.is_regular
  69.972 +            || Scan.unless ($$ "*" -- $$ "}") (Scan.one Symbol.is_regular)) --|
  69.973 +         $$ "*" --| $$ "}" >> (Quote o rd o implode)
  69.974 +      || Scan.repeat1
  69.975 +           (   $$ "'" |-- Scan.one Symbol.is_regular
  69.976 +            || Scan.unless ($$ "_" || $$ "?" || $$ "\<module>" || $$ "/" || $$ "{" |-- $$ "*")
  69.977 +                 (Scan.one Symbol.is_regular)) >> (Pretty o str o implode)))
  69.978 +       (Symbol.explode s) of
  69.979 +     (p, []) => p
  69.980 +   | _ => error ("Malformed annotation: " ^ quote s));
  69.981 +
  69.982 +
  69.983 +val _ = List.app Keyword.keyword ["attach", "file", "contains"];
  69.984 +
  69.985 +fun strip_whitespace s = implode (fst (take_suffix (fn c => c = "\n" orelse c = " ")
  69.986 +  (snd (take_prefix (fn c => c = "\n" orelse c = " ") (raw_explode s))))) ^ "\n";
  69.987 +
  69.988 +val parse_attach = Scan.repeat (Parse.$$$ "attach" |--
  69.989 +  Scan.optional (Parse.$$$ "(" |-- Parse.xname --| Parse.$$$ ")") "" --
  69.990 +    (Parse.verbatim >> strip_whitespace));
  69.991 +
  69.992 +val _ =
  69.993 +  Outer_Syntax.command "types_code"
  69.994 +  "associate types with target language types" Keyword.thy_decl
  69.995 +    (Scan.repeat1 (Parse.xname --| Parse.$$$ "(" -- Parse.string --| Parse.$$$ ")" -- parse_attach) >>
  69.996 +     (fn xs => Toplevel.theory (fn thy => fold (assoc_type o
  69.997 +       (fn ((name, mfx), aux) => (name, (parse_mixfix
  69.998 +         (Syntax.read_typ_global thy) mfx, aux)))) xs thy)));
  69.999 +
 69.1000 +val _ =
 69.1001 +  Outer_Syntax.command "consts_code"
 69.1002 +  "associate constants with target language code" Keyword.thy_decl
 69.1003 +    (Scan.repeat1
 69.1004 +       (Parse.term --|
 69.1005 +        Parse.$$$ "(" -- Parse.string --| Parse.$$$ ")" -- parse_attach) >>
 69.1006 +     (fn xs => Toplevel.theory (fn thy => fold (assoc_const o
 69.1007 +       (fn ((const, mfx), aux) =>
 69.1008 +         (const, (parse_mixfix (Syntax.read_term_global thy) mfx, aux)))) xs thy)));
 69.1009 +
 69.1010 +fun parse_code lib =
 69.1011 +  Scan.optional (Parse.$$$ "(" |-- Parse.enum "," Parse.xname --| Parse.$$$ ")") [] --
 69.1012 +  (if lib then Scan.optional Parse.name "" else Parse.name) --
 69.1013 +  Scan.option (Parse.$$$ "file" |-- Parse.name) --
 69.1014 +  (if lib then Scan.succeed []
 69.1015 +   else Scan.optional (Parse.$$$ "imports" |-- Scan.repeat1 Parse.name) []) --|
 69.1016 +  Parse.$$$ "contains" --
 69.1017 +  (   Scan.repeat1 (Parse.name --| Parse.$$$ "=" -- Parse.term)
 69.1018 +   || Scan.repeat1 (Parse.term >> pair "")) >>
 69.1019 +  (fn ((((mode, module), opt_fname), modules), xs) => Toplevel.theory (fn thy =>
 69.1020 +    let
 69.1021 +      val _ = legacy_feature "Old code generation command -- use 'export_code' instead";
 69.1022 +      val mode' = (if lib then insert (op =) "library" else I) (remove (op =) "library" mode);
 69.1023 +      val (code, gr) = generate_code thy mode' modules module xs;
 69.1024 +      val thy' = thy |> Context.theory_map (ML_Context.exec (fn () =>
 69.1025 +        (case opt_fname of
 69.1026 +          NONE => ML_Context.eval_text false Position.none (cat_lines (map snd code))
 69.1027 +        | SOME fname =>
 69.1028 +            if lib then app (fn (name, s) => File.write
 69.1029 +                (Path.append (Path.explode fname) (Path.basic (name ^ ".ML"))) s)
 69.1030 +              (("ROOT", implode (map (fn (name, _) =>
 69.1031 +                  "use \"" ^ name ^ ".ML\";\n") code)) :: code)
 69.1032 +            else File.write (Path.explode fname) (snd (hd code)))));
 69.1033 +    in
 69.1034 +      if lib then thy'
 69.1035 +      else map_modules (Symtab.update (module, gr)) thy'
 69.1036 +    end));
 69.1037 +
 69.1038 +val setup = add_codegen "default" default_codegen
 69.1039 +  #> add_tycodegen "default" default_tycodegen
 69.1040 +  #> add_preprocessor unfold_preprocessor;
 69.1041 +
 69.1042 +val _ =
 69.1043 +  Outer_Syntax.command "code_library"
 69.1044 +    "generate code for terms (one structure for each theory)" Keyword.thy_decl
 69.1045 +    (parse_code true);
 69.1046 +
 69.1047 +val _ =
 69.1048 +  Outer_Syntax.command "code_module"
 69.1049 +    "generate code for terms (single structure, incremental)" Keyword.thy_decl
 69.1050 +    (parse_code false);
 69.1051 +
 69.1052 +end;
    70.1 --- a/src/Tools/misc_legacy.ML	Wed Aug 10 18:02:16 2011 -0700
    70.2 +++ b/src/Tools/misc_legacy.ML	Wed Aug 10 18:07:32 2011 -0700
    70.3 @@ -5,6 +5,22 @@
    70.4  
    70.5  signature MISC_LEGACY =
    70.6  sig
    70.7 +  val it_term_types: (typ * 'a -> 'a) -> term * 'a -> 'a
    70.8 +  val add_term_names: term * string list -> string list
    70.9 +  val add_typ_tvars: typ * (indexname * sort) list -> (indexname * sort) list
   70.10 +  val add_typ_tfree_names: typ * string list -> string list
   70.11 +  val add_typ_tfrees: typ * (string * sort) list -> (string * sort) list
   70.12 +  val add_term_tvars: term * (indexname * sort) list -> (indexname * sort) list
   70.13 +  val add_term_tfrees: term * (string * sort) list -> (string * sort) list
   70.14 +  val add_term_tfree_names: term * string list -> string list
   70.15 +  val typ_tfrees: typ -> (string * sort) list
   70.16 +  val typ_tvars: typ -> (indexname * sort) list
   70.17 +  val term_tfrees: term -> (string * sort) list
   70.18 +  val term_tvars: term -> (indexname * sort) list
   70.19 +  val add_term_vars: term * term list -> term list
   70.20 +  val term_vars: term -> term list
   70.21 +  val add_term_frees: term * term list -> term list
   70.22 +  val term_frees: term -> term list
   70.23    val mk_defpair: term * term -> string * term
   70.24    val get_def: theory -> xstring -> thm
   70.25    val simple_read_term: theory -> typ -> string -> term
   70.26 @@ -14,6 +30,71 @@
   70.27  structure Misc_Legacy: MISC_LEGACY =
   70.28  struct
   70.29  
   70.30 +(*iterate a function over all types in a term*)
   70.31 +fun it_term_types f =
   70.32 +let fun iter(Const(_,T), a) = f(T,a)
   70.33 +      | iter(Free(_,T), a) = f(T,a)
   70.34 +      | iter(Var(_,T), a) = f(T,a)
   70.35 +      | iter(Abs(_,T,t), a) = iter(t,f(T,a))
   70.36 +      | iter(f$u, a) = iter(f, iter(u, a))
   70.37 +      | iter(Bound _, a) = a
   70.38 +in iter end
   70.39 +
   70.40 +(*Accumulates the names in the term, suppressing duplicates.
   70.41 +  Includes Frees and Consts.  For choosing unambiguous bound var names.*)
   70.42 +fun add_term_names (Const(a,_), bs) = insert (op =) (Long_Name.base_name a) bs
   70.43 +  | add_term_names (Free(a,_), bs) = insert (op =) a bs
   70.44 +  | add_term_names (f$u, bs) = add_term_names (f, add_term_names(u, bs))
   70.45 +  | add_term_names (Abs(_,_,t), bs) = add_term_names(t,bs)
   70.46 +  | add_term_names (_, bs) = bs;
   70.47 +
   70.48 +(*Accumulates the TVars in a type, suppressing duplicates.*)
   70.49 +fun add_typ_tvars(Type(_,Ts),vs) = List.foldr add_typ_tvars vs Ts
   70.50 +  | add_typ_tvars(TFree(_),vs) = vs
   70.51 +  | add_typ_tvars(TVar(v),vs) = insert (op =) v vs;
   70.52 +
   70.53 +(*Accumulates the TFrees in a type, suppressing duplicates.*)
   70.54 +fun add_typ_tfree_names(Type(_,Ts),fs) = List.foldr add_typ_tfree_names fs Ts
   70.55 +  | add_typ_tfree_names(TFree(f,_),fs) = insert (op =) f fs
   70.56 +  | add_typ_tfree_names(TVar(_),fs) = fs;
   70.57 +
   70.58 +fun add_typ_tfrees(Type(_,Ts),fs) = List.foldr add_typ_tfrees fs Ts
   70.59 +  | add_typ_tfrees(TFree(f),fs) = insert (op =) f fs
   70.60 +  | add_typ_tfrees(TVar(_),fs) = fs;
   70.61 +
   70.62 +(*Accumulates the TVars in a term, suppressing duplicates.*)
   70.63 +val add_term_tvars = it_term_types add_typ_tvars;
   70.64 +
   70.65 +(*Accumulates the TFrees in a term, suppressing duplicates.*)
   70.66 +val add_term_tfrees = it_term_types add_typ_tfrees;
   70.67 +val add_term_tfree_names = it_term_types add_typ_tfree_names;
   70.68 +
   70.69 +(*Non-list versions*)
   70.70 +fun typ_tfrees T = add_typ_tfrees(T,[]);
   70.71 +fun typ_tvars T = add_typ_tvars(T,[]);
   70.72 +fun term_tfrees t = add_term_tfrees(t,[]);
   70.73 +fun term_tvars t = add_term_tvars(t,[]);
   70.74 +
   70.75 +
   70.76 +(*Accumulates the Vars in the term, suppressing duplicates.*)
   70.77 +fun add_term_vars (t, vars: term list) = case t of
   70.78 +    Var   _ => Ord_List.insert Term_Ord.term_ord t vars
   70.79 +  | Abs (_,_,body) => add_term_vars(body,vars)
   70.80 +  | f$t =>  add_term_vars (f, add_term_vars(t, vars))
   70.81 +  | _ => vars;
   70.82 +
   70.83 +fun term_vars t = add_term_vars(t,[]);
   70.84 +
   70.85 +(*Accumulates the Frees in the term, suppressing duplicates.*)
   70.86 +fun add_term_frees (t, frees: term list) = case t of
   70.87 +    Free   _ => Ord_List.insert Term_Ord.term_ord t frees
   70.88 +  | Abs (_,_,body) => add_term_frees(body,frees)
   70.89 +  | f$t =>  add_term_frees (f, add_term_frees(t, frees))
   70.90 +  | _ => frees;
   70.91 +
   70.92 +fun term_frees t = add_term_frees(t,[]);
   70.93 +
   70.94 +
   70.95  fun mk_defpair (lhs, rhs) =
   70.96    (case Term.head_of lhs of
   70.97      Const (name, _) =>
    71.1 --- a/src/ZF/Tools/inductive_package.ML	Wed Aug 10 18:02:16 2011 -0700
    71.2 +++ b/src/ZF/Tools/inductive_package.ML	Wed Aug 10 18:07:32 2011 -0700
    71.3 @@ -96,7 +96,7 @@
    71.4                 Syntax.string_of_term ctxt t);
    71.5  
    71.6    (*** Construct the fixedpoint definition ***)
    71.7 -  val mk_variant = singleton (Name.variant_list (List.foldr OldTerm.add_term_names [] intr_tms));
    71.8 +  val mk_variant = singleton (Name.variant_list (List.foldr Misc_Legacy.add_term_names [] intr_tms));
    71.9  
   71.10    val z' = mk_variant"z" and X' = mk_variant"X" and w' = mk_variant"w";
   71.11  
   71.12 @@ -108,7 +108,7 @@
   71.13    fun fp_part intr = (*quantify over rule's free vars except parameters*)
   71.14      let val prems = map dest_tprop (Logic.strip_imp_prems intr)
   71.15          val dummy = List.app (fn rec_hd => List.app (Ind_Syntax.chk_prem rec_hd) prems) rec_hds
   71.16 -        val exfrees = subtract (op =) rec_params (OldTerm.term_frees intr)
   71.17 +        val exfrees = subtract (op =) rec_params (Misc_Legacy.term_frees intr)
   71.18          val zeq = FOLogic.mk_eq (Free(z', Ind_Syntax.iT), #1 (Ind_Syntax.rule_concl intr))
   71.19      in List.foldr FOLogic.mk_exists
   71.20               (Balanced_Tree.make FOLogic.mk_conj (zeq::prems)) exfrees
   71.21 @@ -296,7 +296,7 @@
   71.22  
   71.23       (*Make a premise of the induction rule.*)
   71.24       fun induct_prem ind_alist intr =
   71.25 -       let val quantfrees = map dest_Free (subtract (op =) rec_params (OldTerm.term_frees intr))
   71.26 +       let val quantfrees = map dest_Free (subtract (op =) rec_params (Misc_Legacy.term_frees intr))
   71.27             val iprems = List.foldr (add_induct_prem ind_alist) []
   71.28                                (Logic.strip_imp_prems intr)
   71.29             val (t,X) = Ind_Syntax.rule_concl intr