src/HOL/Tools/inductive_realizer.ML
changeset 33040 cffdb7b28498
parent 32952 aeb1e44fbc19
child 33171 292970b42770
     1.1 --- a/src/HOL/Tools/inductive_realizer.ML	Wed Oct 21 08:16:25 2009 +0200
     1.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Wed Oct 21 10:15:31 2009 +0200
     1.3 @@ -70,7 +70,7 @@
     1.4      val params = map dest_Var (Library.take (nparms, ts));
     1.5      val tname = Binding.name (space_implode "_" (Long_Name.base_name s ^ "T" :: vs));
     1.6      fun constr_of_intr intr = (Binding.name (Long_Name.base_name (name_of_thm intr)),
     1.7 -      map (Logic.unvarifyT o snd) (rev (Term.add_vars (prop_of intr) []) \\ params) @
     1.8 +      map (Logic.unvarifyT o snd) (subtract (op =) params (rev (Term.add_vars (prop_of intr) []))) @
     1.9          filter_out (equal Extraction.nullT) (map
    1.10            (Logic.unvarifyT o Extraction.etype_of thy vs []) (prems_of intr)),
    1.11              NoSyn);
    1.12 @@ -115,7 +115,7 @@
    1.13      val r = if n then Extraction.nullt else Var ((Long_Name.base_name s, 0), rT);
    1.14      val S = list_comb (h, params @ xs);
    1.15      val rvs = relevant_vars S;
    1.16 -    val vs' = map fst rvs \\ vs;
    1.17 +    val vs' = subtract (op =) vs (map fst rvs);
    1.18      val rname = space_implode "_" (s ^ "R" :: vs);
    1.19  
    1.20      fun mk_Tprem n v =
    1.21 @@ -141,7 +141,7 @@
    1.22      val ctxt = ProofContext.init thy
    1.23      val args = map (Free o apfst fst o dest_Var) ivs;
    1.24      val args' = map (Free o apfst fst)
    1.25 -      (Term.add_vars (prop_of intr) [] \\ params);
    1.26 +      (subtract (op =) params (Term.add_vars (prop_of intr) []));
    1.27      val rule' = strip_all rule;
    1.28      val conclT = Extraction.etype_of thy vs [] (Logic.strip_imp_concl rule');
    1.29      val used = map (fst o dest_Free) args;
    1.30 @@ -331,7 +331,7 @@
    1.31      val rintrs = map (fn (intr, c) => Envir.eta_contract
    1.32        (Extraction.realizes_of thy2 vs
    1.33          (if c = Extraction.nullt then c else list_comb (c, map Var (rev
    1.34 -          (Term.add_vars (prop_of intr) []) \\ params'))) (prop_of intr)))
    1.35 +          (subtract (op =) params' (Term.add_vars (prop_of intr) []))))) (prop_of intr)))
    1.36              (maps snd rss ~~ flat constrss);
    1.37      val (rlzpreds, rlzpreds') =
    1.38        rintrs |> map (fn rintr =>
    1.39 @@ -427,9 +427,9 @@
    1.40          val (prem :: prems) = prems_of elim;
    1.41          fun reorder1 (p, (_, intr)) =
    1.42            Library.foldl (fn (t, ((s, _), T)) => Logic.all (Free (s, T)) t)
    1.43 -            (strip_all p, Term.add_vars (prop_of intr) [] \\ params');
    1.44 +            (strip_all p, subtract (op =) params' (Term.add_vars (prop_of intr) []));
    1.45          fun reorder2 ((ivs, intr), i) =
    1.46 -          let val fs = Term.add_vars (prop_of intr) [] \\ params'
    1.47 +          let val fs = subtract (op =) params' (Term.add_vars (prop_of intr) [])
    1.48            in Library.foldl (fn (t, x) => lambda (Var x) t)
    1.49              (list_comb (Bound (i + length ivs), ivs), fs)
    1.50            end;
    1.51 @@ -469,7 +469,7 @@
    1.52      val thy5 = Extraction.add_realizers_i
    1.53        (map (mk_realizer thy4 vs) (map (fn (((rule, rrule), rlz), c) =>
    1.54           (name_of_thm rule, rule, rrule, rlz,
    1.55 -            list_comb (c, map Var (rev (Term.add_vars (prop_of rule) []) \\ params'))))
    1.56 +            list_comb (c, map Var (subtract (op =) params' (rev (Term.add_vars (prop_of rule) []))))))
    1.57                (maps snd rss ~~ #intrs ind_info ~~ rintrs ~~ flat constrss))) thy4;
    1.58      val elimps = map_filter (fn ((s, intrs), p) =>
    1.59        if s mem rsets then SOME (p, intrs) else NONE)
    1.60 @@ -503,7 +503,7 @@
    1.61      add_ind_realizers (hd sets)
    1.62        (case arg of
    1.63          NONE => sets | SOME NONE => []
    1.64 -      | SOME (SOME sets') => sets \\ sets')
    1.65 +      | SOME (SOME sets') => subtract (op =) sets' sets)
    1.66    end I);
    1.67  
    1.68  val setup =