tuned;
authorwenzelm
Sat Mar 10 17:07:10 2012 +0100 (2012-03-10 ago)
changeset 4685628909eecdf5b
parent 46855 f72a2bedd7a9
child 46857 628b4a3fbf6e
tuned;
src/Pure/Isar/class_declaration.ML
src/Pure/Isar/element.ML
src/Pure/Isar/expression.ML
     1.1 --- a/src/Pure/Isar/class_declaration.ML	Sat Mar 10 16:49:34 2012 +0100
     1.2 +++ b/src/Pure/Isar/class_declaration.ML	Sat Mar 10 17:07:10 2012 +0100
     1.3 @@ -74,13 +74,12 @@
     1.4          val ((_, [thm']), _) = Variable.import true [thm] empty_ctxt;
     1.5          val const_eq_morph =
     1.6            (case eq_morph of
     1.7 -             SOME eq_morph => const_morph $> eq_morph
     1.8 +            SOME eq_morph => const_morph $> eq_morph
     1.9            | NONE => const_morph);
    1.10          val thm'' = Morphism.thm const_eq_morph thm';
    1.11          val tac = ALLGOALS (Proof_Context.fact_tac [thm'']);
    1.12        in Skip_Proof.prove_global thy [] [] (Thm.prop_of thm'') (K tac) end;
    1.13 -    val assm_intro = Option.map prove_assm_intro
    1.14 -      (fst (Locale.intros_of thy class));
    1.15 +    val assm_intro = Option.map prove_assm_intro (fst (Locale.intros_of thy class));
    1.16  
    1.17      (* of_class *)
    1.18      val of_class_prop_concl = Logic.mk_of_class (aT, class);
     2.1 --- a/src/Pure/Isar/element.ML	Sat Mar 10 16:49:34 2012 +0100
     2.2 +++ b/src/Pure/Isar/element.ML	Sat Mar 10 17:07:10 2012 +0100
     2.3 @@ -461,11 +461,13 @@
     2.4  
     2.5  (* rewriting with equalities *)
     2.6  
     2.7 -fun eq_morphism thy thms = if null thms then NONE else SOME (Morphism.morphism
     2.8 - {binding = [],
     2.9 -  typ = [],
    2.10 -  term = [Raw_Simplifier.rewrite_term thy thms []],
    2.11 -  fact = [map (Raw_Simplifier.rewrite_rule thms)]});
    2.12 +fun eq_morphism _ [] = NONE
    2.13 +  | eq_morphism thy thms =
    2.14 +      SOME (Morphism.morphism
    2.15 +       {binding = [],
    2.16 +        typ = [],
    2.17 +        term = [Raw_Simplifier.rewrite_term thy thms []],
    2.18 +        fact = [map (Raw_Simplifier.rewrite_rule thms)]});
    2.19  
    2.20  
    2.21  (* transfer to theory using closure *)
     3.1 --- a/src/Pure/Isar/expression.ML	Sat Mar 10 16:49:34 2012 +0100
     3.2 +++ b/src/Pure/Isar/expression.ML	Sat Mar 10 17:07:10 2012 +0100
     3.3 @@ -899,8 +899,7 @@
     3.4      |> Proof_Context.background_theory (fold (fn ((dep, morph), wits) =>
     3.5        fn thy =>
     3.6          Locale.add_dependency target
     3.7 -          (dep, morph $> Element.satisfy_morphism
     3.8 -            (map (Element.transform_witness export') wits))
     3.9 +          (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits))
    3.10            (Element.eq_morphism thy eqns' |> Option.map (rpair true))
    3.11            export thy) (deps ~~ witss))
    3.12    end;