src/HOL/Tools/refute.ML
changeset 22055 7c81de75d2c3
parent 22024 adf64b316f07
child 22092 ab3dfcef6489
equal deleted inserted replaced
22054:4cb2fe751952 22055:7c81de75d2c3
  1231 (* ------------------------------------------------------------------------- *)
  1231 (* ------------------------------------------------------------------------- *)
  1232 
  1232 
  1233 	(* theory -> (string * string) list -> Thm.thm -> int -> unit *)
  1233 	(* theory -> (string * string) list -> Thm.thm -> int -> unit *)
  1234 
  1234 
  1235 	fun refute_subgoal thy params thm subgoal =
  1235 	fun refute_subgoal thy params thm subgoal =
  1236 		refute_term thy params (List.nth (prems_of thm, subgoal));
  1236 		refute_term thy params (List.nth (Thm.prems_of thm, subgoal));
  1237 
  1237 
  1238 
  1238 
  1239 (* ------------------------------------------------------------------------- *)
  1239 (* ------------------------------------------------------------------------- *)
  1240 (* INTERPRETERS: Auxiliary Functions                                         *)
  1240 (* INTERPRETERS: Auxiliary Functions                                         *)
  1241 (* ------------------------------------------------------------------------- *)
  1241 (* ------------------------------------------------------------------------- *)