src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
changeset 58341 6c8b30b9f583
parent 58142 d6a2e3567f95
child 58342 9a82544fd29f
equal deleted inserted replaced
58340:5f6f48e87de6 58341:6c8b30b9f583
   166           (case compress of
   166           (case compress of
   167             NONE => if isar_proofs = NONE andalso do_preplay then 1000.0 else 10.0
   167             NONE => if isar_proofs = NONE andalso do_preplay then 1000.0 else 10.0
   168           | SOME n => n)
   168           | SOME n => n)
   169 
   169 
   170         fun is_fixed ctxt = Variable.is_declared ctxt orf Name.is_skolem
   170         fun is_fixed ctxt = Variable.is_declared ctxt orf Name.is_skolem
   171         fun skolems_of ctxt t = Term.add_frees t [] |> filter_out (is_fixed ctxt o fst) |> rev |> @{print}
   171         fun skolems_of ctxt t = Term.add_frees t [] |> filter_out (is_fixed ctxt o fst) |> rev
   172 
   172 
   173         fun get_role keep_role ((num, _), role, t, rule, _) =
   173         fun get_role keep_role ((num, _), role, t, rule, _) =
   174           if keep_role role then SOME ((raw_label_of_num num, t), rule) else NONE
   174           if keep_role role then SOME ((raw_label_of_num num, t), rule) else NONE
   175 
   175 
   176         val atp_proof =
   176         val atp_proof =