src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
changeset 37145 01aa36932739
parent 36968 62e29faa3718
child 37146 f652333bbf8e
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Thu May 27 15:28:23 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Thu May 27 17:41:27 2010 +0200
     1.3 @@ -254,7 +254,7 @@
     1.4              SOME b => TVar (("'" ^ b, 0), HOLogic.typeS)
     1.5            | NONE =>
     1.6              (* Variable from the ATP, say "X1" *)
     1.7 -            TypeInfer.param 0 (a, HOLogic.typeS)
     1.8 +            Type_Infer.param 0 (a, HOLogic.typeS)
     1.9      end
    1.10  
    1.11  (*Invert the table of translations between Isabelle and ATPs*)
    1.12 @@ -453,7 +453,7 @@
    1.13      val (vt, t) = lits_of_nodes thy full_types tfrees (Vartab.empty, []) us
    1.14    in repair_tvar_sorts vt t end
    1.15  fun check_formula ctxt =
    1.16 -  TypeInfer.constrain @{typ bool}
    1.17 +  Type_Infer.constrain @{typ bool}
    1.18    #> Syntax.check_term (ProofContext.set_mode ProofContext.mode_schematic ctxt)
    1.19  
    1.20