src/HOL/Tools/Nitpick/minipick.ML
changeset 35185 9b8f351cced6
parent 35028 108662d50512
child 35280 54ab4921f826
     1.1 --- a/src/HOL/Tools/Nitpick/minipick.ML	Wed Feb 17 11:20:09 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/minipick.ML	Wed Feb 17 12:14:08 2010 +0100
     1.3 @@ -84,7 +84,7 @@
     1.4  fun atom_from_formula f = RelIf (f, true_atom, false_atom)
     1.5  
     1.6  (* Proof.context -> (typ -> int) -> styp list -> term -> formula *)
     1.7 -fun kodkod_formula_for_term ctxt card frees =
     1.8 +fun kodkod_formula_from_term ctxt card frees =
     1.9    let
    1.10      (* typ -> rel_expr -> rel_expr *)
    1.11      fun R_rep_from_S_rep (T as Type ("fun", [T1, @{typ bool}])) r =
    1.12 @@ -145,7 +145,7 @@
    1.13         | Term.Var _ => raise SAME ()
    1.14         | Bound _ => raise SAME ()
    1.15         | Const (s, _) => raise NOT_SUPPORTED ("constant " ^ quote s)
    1.16 -       | _ => raise TERM ("Minipick.kodkod_formula_for_term.to_F", [t]))
    1.17 +       | _ => raise TERM ("Minipick.kodkod_formula_from_term.to_F", [t]))
    1.18        handle SAME () => formula_from_atom (to_R_rep Ts t)
    1.19      (* typ list -> term -> rel_expr *)
    1.20      and to_S_rep Ts t =
    1.21 @@ -306,7 +306,7 @@
    1.22      val bounds = map2 (bound_for_free card) (index_seq 0 (length frees)) frees
    1.23      val declarative_axioms =
    1.24        map2 (declarative_axiom_for_free card) (index_seq 0 (length frees)) frees
    1.25 -    val formula = kodkod_formula_for_term ctxt card frees neg_t
    1.26 +    val formula = kodkod_formula_from_term ctxt card frees neg_t
    1.27                    |> fold_rev (curry And) declarative_axioms
    1.28      val univ_card = univ_card 0 0 0 bounds formula
    1.29      val problem =