src/HOL/Tools/refute.ML
changeset 42361 23f352990944
parent 42137 6803f2fd15c1
child 42364 8c674b3b8e44
     1.1 --- a/src/HOL/Tools/refute.ML	Sat Apr 16 15:47:52 2011 +0200
     1.2 +++ b/src/HOL/Tools/refute.ML	Sat Apr 16 16:15:37 2011 +0200
     1.3 @@ -224,7 +224,7 @@
     1.4       parameters = Symtab.merge (op =) (pa1, pa2)};
     1.5  );
     1.6  
     1.7 -val get_data = Data.get o ProofContext.theory_of;
     1.8 +val get_data = Data.get o Proof_Context.theory_of;
     1.9  
    1.10  
    1.11  (* ------------------------------------------------------------------------- *)
    1.12 @@ -683,7 +683,7 @@
    1.13  
    1.14  fun collect_axioms ctxt t =
    1.15    let
    1.16 -    val thy = ProofContext.theory_of ctxt
    1.17 +    val thy = Proof_Context.theory_of ctxt
    1.18      val _ = tracing "Adding axioms..."
    1.19      val axioms = Theory.all_axioms_of thy
    1.20      fun collect_this_axiom (axname, ax) axs =
    1.21 @@ -858,7 +858,7 @@
    1.22  
    1.23  fun ground_types ctxt t =
    1.24    let
    1.25 -    val thy = ProofContext.theory_of ctxt
    1.26 +    val thy = Proof_Context.theory_of ctxt
    1.27      fun collect_types T acc =
    1.28        (case T of
    1.29          Type ("fun", [T1, T2]) => collect_types T1 (collect_types T2 acc)
    1.30 @@ -1049,7 +1049,7 @@
    1.31      {sizes, minsize, maxsize, maxvars, maxtime, satsolver, no_assms, expect}
    1.32      assm_ts t negate =
    1.33    let
    1.34 -    val thy = ProofContext.theory_of ctxt
    1.35 +    val thy = Proof_Context.theory_of ctxt
    1.36      (* string -> unit *)
    1.37      fun check_expect outcome_code =
    1.38        if expect = "" orelse outcome_code = expect then ()
    1.39 @@ -1548,7 +1548,7 @@
    1.40  
    1.41  fun stlc_interpreter ctxt model args t =
    1.42    let
    1.43 -    val thy = ProofContext.theory_of ctxt
    1.44 +    val thy = Proof_Context.theory_of ctxt
    1.45      val (typs, terms) = model
    1.46      val {maxvars, def_eq, next_idx, bounds, wellformed} = args
    1.47      (* Term.typ -> (interpretation * model * arguments) option *)
    1.48 @@ -1836,7 +1836,7 @@
    1.49  
    1.50  fun IDT_interpreter ctxt model args t =
    1.51    let
    1.52 -    val thy = ProofContext.theory_of ctxt
    1.53 +    val thy = Proof_Context.theory_of ctxt
    1.54      val (typs, terms) = model
    1.55      (* Term.typ -> (interpretation * model * arguments) option *)
    1.56      fun interpret_term (Type (s, Ts)) =
    1.57 @@ -1929,7 +1929,7 @@
    1.58  
    1.59  fun IDT_constructor_interpreter ctxt model args t =
    1.60    let
    1.61 -    val thy = ProofContext.theory_of ctxt
    1.62 +    val thy = Proof_Context.theory_of ctxt
    1.63      (* returns a list of canonical representations for terms of the type 'T' *)
    1.64      (* It would be nice if we could just use 'print' for this, but 'print'   *)
    1.65      (* for IDTs calls 'IDT_constructor_interpreter' again, and this could    *)
    1.66 @@ -2194,7 +2194,7 @@
    1.67  
    1.68  fun IDT_recursion_interpreter ctxt model args t =
    1.69    let
    1.70 -    val thy = ProofContext.theory_of ctxt
    1.71 +    val thy = Proof_Context.theory_of ctxt
    1.72    in
    1.73      (* careful: here we descend arbitrarily deep into 't', possibly before *)
    1.74      (* any other interpreter for atomic terms has had a chance to look at  *)
    1.75 @@ -3022,7 +3022,7 @@
    1.76  
    1.77  fun IDT_printer ctxt model T intr assignment =
    1.78    let
    1.79 -    val thy = ProofContext.theory_of ctxt
    1.80 +    val thy = Proof_Context.theory_of ctxt
    1.81    in
    1.82      (case T of
    1.83        Type (s, Ts) =>
    1.84 @@ -3189,7 +3189,7 @@
    1.85          let
    1.86            val thy' = fold set_default_param parms thy;
    1.87            val output =
    1.88 -            (case get_default_params (ProofContext.init_global thy') of
    1.89 +            (case get_default_params (Proof_Context.init_global thy') of
    1.90                [] => "none"
    1.91              | new_defaults => cat_lines (map (fn (x, y) => x ^ "=" ^ y) new_defaults));
    1.92            val _ = writeln ("Default parameters for 'refute':\n" ^ output);