src/Pure/Tools/find_theorems.ML
changeset 43620 43a195a0279b
parent 43076 7b06cd71792c
child 43724 4e58485fa320
     1.1 --- a/src/Pure/Tools/find_theorems.ML	Fri Jul 01 15:16:03 2011 +0200
     1.2 +++ b/src/Pure/Tools/find_theorems.ML	Fri Jul 01 16:05:38 2011 +0200
     1.3 @@ -101,6 +101,7 @@
     1.4    end;
     1.5  
     1.6  
     1.7 +
     1.8  (** queries **)
     1.9  
    1.10  type 'term query = {
    1.11 @@ -154,6 +155,8 @@
    1.12        end
    1.13    | query_of_xml tree = raise XML_Syntax.XML ("query_of_xml: bad tree", tree);
    1.14  
    1.15 +
    1.16 +
    1.17  (** theorems, either internal or external (without proof) **)
    1.18  
    1.19  datatype theorem =
    1.20 @@ -164,21 +167,21 @@
    1.21        Position.markup pos o Markup.properties [("name", name), ("index", Markup.print_int i)]
    1.22    | fact_ref_markup (Facts.Named ((name, pos), NONE)) =
    1.23        Position.markup pos o Markup.properties [("name", name)]
    1.24 -  | fact_ref_markup fact_ref = raise Fail "bad fact ref"
    1.25 +  | fact_ref_markup fact_ref = raise Fail "bad fact ref";
    1.26  
    1.27  fun xml_of_theorem (Internal _) = raise Fail "xml_of_theorem: Internal"
    1.28    | xml_of_theorem (External (fact_ref, prop)) =
    1.29 -      XML.Elem (fact_ref_markup fact_ref ("External", []), [XML_Syntax.xml_of_term prop])
    1.30 +      XML.Elem (fact_ref_markup fact_ref ("External", []), [XML_Syntax.xml_of_term prop]);
    1.31  
    1.32  fun theorem_of_xml (XML.Elem (("External", properties), [tree])) =
    1.33 -    let
    1.34 -      val name = the (Properties.get properties "name");
    1.35 -      val pos = Position.of_properties properties;
    1.36 -      val intvs_opt = Option.map (single o Facts.Single o Markup.parse_int)
    1.37 -        (Properties.get properties "index");
    1.38 -    in
    1.39 -      External (Facts.Named ((name, pos), intvs_opt), XML_Syntax.term_of_xml tree)
    1.40 -    end
    1.41 +      let
    1.42 +        val name = the (Properties.get properties "name");
    1.43 +        val pos = Position.of_properties properties;
    1.44 +        val intvs_opt = Option.map (single o Facts.Single o Markup.parse_int)
    1.45 +          (Properties.get properties "index");
    1.46 +      in
    1.47 +        External (Facts.Named ((name, pos), intvs_opt), XML_Syntax.term_of_xml tree)
    1.48 +      end
    1.49    | theorem_of_xml tree = raise XML_Syntax.XML ("theorem_of_xml: bad tree", tree);
    1.50  
    1.51  fun xml_of_result (opt_found, theorems) =
    1.52 @@ -207,6 +210,8 @@
    1.53  fun fact_ref_of (Internal (fact_ref, _)) = fact_ref
    1.54    | fact_ref_of (External (fact_ref, _)) = fact_ref;
    1.55  
    1.56 +
    1.57 +
    1.58  (** search criterion filters **)
    1.59  
    1.60  (*generated filters are to be of the form
    1.61 @@ -228,7 +233,7 @@
    1.62  
    1.63  fun is_nontrivial thy = Term.is_Const o Term.head_of o Object_Logic.drop_judgment thy;
    1.64  
    1.65 -(*educated guesses on HOL*)  (* FIXME broken *)
    1.66 +(*educated guesses on HOL*)  (* FIXME utterly broken *)
    1.67  val boolT = Type ("bool", []);
    1.68  val iff_const = Const ("op =", boolT --> boolT --> boolT);
    1.69  
    1.70 @@ -339,8 +344,8 @@
    1.71        else (etacn thm THEN_ALL_NEW (Goal.norm_hhf_tac THEN' Method.assm_tac ctxt)) 1 goal;
    1.72    in
    1.73      fn Internal (_, thm) =>
    1.74 -      if is_some (Seq.pull (try_thm thm))
    1.75 -      then SOME (Thm.nprems_of thm, 0) else NONE
    1.76 +        if is_some (Seq.pull (try_thm thm))
    1.77 +        then SOME (Thm.nprems_of thm, 0) else NONE
    1.78       | External _ => NONE
    1.79    end;
    1.80  
    1.81 @@ -423,7 +428,6 @@
    1.82            in app (opt_add r r', consts', fs) end;
    1.83    in app end;
    1.84  
    1.85 -
    1.86  in
    1.87  
    1.88  fun filter_criterion ctxt opt_goal (b, c) =
    1.89 @@ -520,8 +524,6 @@
    1.90    in
    1.91      maps Facts.selections
    1.92       (visible_facts (Global_Theory.facts_of (Proof_Context.theory_of ctxt)) @
    1.93 -
    1.94 -
    1.95        visible_facts (Proof_Context.facts_of ctxt))
    1.96    end;
    1.97